let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
( L1 is being_line & L2 is being_line )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 // L2 implies ( L1 is being_line & L2 is being_line ) )
assume L1 // L2 ; :: thesis: ( L1 is being_line & L2 is being_line )
then consider x1, x2, y1, y2 being Element of REAL n such that
A1: ( L1 = Line (x1,x2) & L2 = Line (y1,y2) ) and
A2: x2 - x1 // y2 - y1 ;
y2 - y1 <> 0* n by A2;
then A3: y2 <> y1 by Th9;
x2 - x1 <> 0* n by A2;
then x2 <> x1 by Th9;
hence ( L1 is being_line & L2 is being_line ) by A1, A3; :: thesis: verum