let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
L1 <> L2
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 _|_ L2 implies L1 <> L2 )
assume A1: L1 _|_ L2 ; :: thesis: L1 <> L2

now :: thesis: ( ( L1 misses L2 & L1 <> L2 ) or ( L1 meets L2 & L1 <> L2 ) )

per cases ( L1 misses L2 or L1 meets L2 ) ;

case A2: L1 misses L2 ; :: thesis: L1 <> L2

ex x being Element of REAL n st x in L1 by Th52;
hence L1 <> L2 by A2, Th49; :: thesis: verum

end;

case L1 meets L2 ; :: thesis: L1 <> L2

then consider x0 being Element of REAL n such that
A3: x0 in L1 and
A4: x0 in L2 by Th49;
L1 is being_line by A1, Th67;
then consider x1 being Element of REAL n such that
A5: x1 <> x0 and
A6: x1 in L1 by Th53;
A7: x1 - x0 <> 0* n by A5, Th9;
L2 is being_line by A1, Th67;
then consider x2 being Element of REAL n such that
A8: x2 <> x0 and
A9: x2 in L2 by Th53;
A10: x2 - x0 <> 0* n by A8, Th9;
A11: x1 - x0 _|_ x2 - x0 by A1, A3, A4, A5, A6, A8, A9, Th74;
not x1 in L2

proof

assume x1 in L2 ; :: thesis: contradiction
then ex a being Real st x1 - x0 = a * (x2 - x0) by A4, A8, A9, Th70;
then x1 - x0 // x2 - x0 by A7, A10;
hence contradiction by A11, Lm3, Th45; :: thesis: verum

end;

hence L1 <> L2 by A6; :: thesis: verum

end;

end;

end;

hence L1 <> L2 ; :: thesis: verum