let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 is being_line & L2 is being_line & L1 <> L2 implies ex x being Element of REAL n st
( x in L1 & not x in L2 ) )
assume that
A1: L1 is being_line and
A2: L2 is being_line ; :: thesis: ( not L1 <> L2 or ex x being Element of REAL n st
( x in L1 & not x in L2 ) )
consider x1, x2 being Element of REAL n such that
A3: x1 <> x2 and
A4: L1 = Line (x1,x2) by A1;
assume A5: L1 <> L2 ; :: thesis: ex x being Element of REAL n st
( x in L1 & not x in L2 )
now :: thesis: ( ( not x1 in L2 & x1 in L1 & not x1 in L2 ) or ( not x2 in L2 & x2 in L1 & not x2 in L2 ) )
per cases ( not x1 in L2 or not x2 in L2 ) by A2, A3, A4, A5, Th30;
case A6: not x1 in L2 ; :: thesis: ( x1 in L1 & not x1 in L2 )
set x = x1;
thus ( x1 in L1 & not x1 in L2 ) by A4, A6, EUCLID_4:9; :: thesis: verum
end;
case A7: not x2 in L2 ; :: thesis: ( x2 in L1 & not x2 in L2 )
set x = x2;
thus ( x2 in L1 & not x2 in L2 ) by A4, A7, EUCLID_4:9; :: thesis: verum
end;
end;
end;
hence ex x being Element of REAL n st
( x in L1 & not x in L2 ) ; :: thesis: verum