let n be Nat; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
L1,L2 are_coplane
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 // L2 implies L1,L2 are_coplane )
assume L1 // L2 ; :: thesis: L1,L2 are_coplane
then consider x1, x2, y1, y2 being Element of REAL n such that
A1: L1 = Line (x1,x2) and
A2: L2 = Line (y1,y2) and
A3: x2 - x1 // y2 - y1 ;
consider a being Real such that
a <> 0 and
A4: x2 - x1 = a * (y2 - y1) by A3, Th32;
A5: (1 + (- a)) + a = 1 ;
( y1 in plane (x1,y1,y2) & y2 in plane (x1,y1,y2) ) by Th82;
then A6: L2 c= plane (x1,y1,y2) by A2, Th85;
x2 = x1 + (a * (y2 - y1)) by A4, Th6
.= (1 * x1) + (a * (y2 - y1)) by EUCLID_4:3
.= (1 * x1) + ((a * y2) + ((- a) * y1)) by Th12
.= ((1 * x1) + ((- a) * y1)) + (a * y2) by RVSUM_1:15 ;
then A7: x2 in plane (x1,y1,y2) by A5;
x1 in plane (x1,y1,y2) by Th82;
then L1 c= plane (x1,y1,y2) by A1, A7, Th85;
hence L1,L2 are_coplane by A6; :: thesis: verum