# [isabelle] proof by contradiction

hello,
please can anyone help me with a hint of our to prove this codes with by
contradiction.
======================================
theory testing2 imports "~~/src/HOL/Main" begin
locale geometry =
fixes parallel :: "'line ⇒ 'line ⇒ bool"
and intersect :: "'line ⇒ 'line ⇒ bool"
and angle :: "'line ⇒ 'line ⇒ nat"
assumes axiom1: "parallel l1 l2 ⟹ angle l1 l2 = 0"
and axiom2: "intersect l1 l2 ⟹ ¬ (angle l1 l2 = 0)"
begin
lemma parallel_not_intersect: "parallel l1 l2 ⟹ ¬ intersect l1 l2"
=================================================
thanks
Adamu

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*