let n be Element of 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 & x2 - x1 // y2 - y1 ) by Def7;
( x2 - x1 <> 0* n & y2 - y1 <> 0* n ) by A1, Def1;
then ( x2 <> x1 & y2 <> y1 ) by Th14;
hence ( L1 is being_line & L2 is being_line ) by A1, EUCLID_4:def 2; :: thesis: verum