let n be Element of 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

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

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

consider x being Element of REAL n such that
A3: x in L1 by Th57;
thus L1 <> L2 by A2, A3, Th54; :: thesis: verum

end;

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

then consider x0 being Element of REAL n such that
A4: ( x0 in L1 & x0 in L2 ) by Th54;
A5: ( L1 is being_line & L2 is being_line ) by A1, Th72;
then consider x1 being Element of REAL n such that
A6: ( x1 <> x0 & x1 in L1 ) by A4, Th58;
consider x2 being Element of REAL n such that
A7: ( x2 <> x0 & x2 in L2 ) by A4, A5, Th58;
A8: x1 - x0 _|_ x2 - x0 by A1, A4, A6, A7, Th79;
A9: ( x1 - x0 <> 0* n & x2 - x0 <> 0* n ) by A6, A7, Th14;
not x1 in L2

proof

assume x1 in L2 ; :: thesis: contradiction
then consider a being Real such that
A10: x1 - x0 = a * (x2 - x0) by A4, A7, Th75;
x1 - x0 // x2 - x0 by A9, A10, Def1;
hence contradiction by A8, Lm3, Th50; :: thesis: verum

end;

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

end;

end;

end;

hence L1 <> L2 ; :: thesis: verum