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