let n be Element of NAT ; :: thesis: for x2, x1, x3, y2, y3 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
let x2, x1, x3, y2, y3 be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) implies ( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) )
assume that
A1: x2 - x1,x3 - x1 are_lindependent2 and
A2: y2 in Line (x1,x2) and
A3: y3 in Line (x1,x3) and
A4: L1 = Line (x2,x3) and
A5: L2 = Line (y2,y3) ; :: thesis: ( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
thus ( L1 // L2 implies ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) :: thesis: ( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 )

proof

assume A6: L1 // L2 ; :: thesis: ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
then L1 is being_line by Th71;
then A7: x2 <> x3 by A4, Th81;
L2 is being_line by A6, Th71;
then A8: y2 <> y3 by A5, Th81;
A9: ( y2 in L2 & y3 in L2 ) by A5, EUCLID_4:10;
consider t being Real such that
A10: y3 = ((1 - t) * x1) + (t * x3) by A3;
( x2 in L1 & x3 in L1 ) by A4, EUCLID_4:10;
then A11: y3 - y2 // x3 - x2 by A6, A7, A8, A9, Th82;
then consider a being Real such that
A12: y3 - y2 = a * (x3 - x2) by Def1;
take a ; :: thesis: ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
consider s being Real such that
A13: y2 = ((1 - s) * x1) + (s * x2) by A2;
A14: 0* n = (y3 - y2) - (a * (x3 - x2)) by A12, Th14
.= (((((1 - t) * x1) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2)) by A13, A10, RVSUM_1:60
.= (((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2)) by Th16
.= (((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 * x1) + (- (s * x1)))) - (s * x2)) - (a * (x3 - x2)) by Th16
.= ((((((1 * x1) + (- (t * x1))) + (t * x3)) - (1 * x1)) - (- (s * x1))) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:60
.= ((((((1 * x1) + (- (t * x1))) + (- (1 * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:32
.= ((((((1 * x1) + (- (1 * x1))) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:32
.= (((((0* n) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by Th7
.= ((((- (t * x1)) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by EUCLID_4:1
.= (((t * (x3 - x1)) + (s * x1)) + (- (s * x2))) - (a * (x3 - x2)) by Th17
.= (((t * (x3 - x1)) - (s * x2)) + (s * x1)) - (a * (x3 - x2)) by RVSUM_1:32
.= ((t * (x3 - x1)) - ((s * x2) - (s * x1))) - (a * (x3 - x2)) by Th9
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x2)) by Th17
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (0* n)) - x2)) by RVSUM_1:53
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (x1 - x1)) - x2)) by Th7
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (((x3 - x1) + x1) + (- x2))) by Th9
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - x1) + ((- x2) + x1))) by RVSUM_1:32
.= ((t * (x3 - x1)) - (s * (x2 - x1))) - ((a * (x3 - x1)) + (a * ((- x2) + x1))) by EUCLID_4:6
.= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x1))) - (a * ((- x2) + x1)) by RVSUM_1:60
.= ((t * (x3 - x1)) - ((a * (x3 - x1)) + (s * (x2 - x1)))) - (a * ((- x2) + x1)) by RVSUM_1:60
.= (((t * (x3 - x1)) - (a * (x3 - x1))) - (s * (x2 - x1))) - (a * ((- x2) + x1)) by RVSUM_1:60
.= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (a * ((- x2) + x1)) by Th16
.= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((a * (- x2)) + (a * x1)) by EUCLID_4:6
.= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((- (a * x2)) + (a * x1)) by Th8
.= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (- (a * x2))) - (a * x1) by RVSUM_1:60
.= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) + ((a * x2) + (- (a * x1))) by RVSUM_1:32
.= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) + (a * (x2 - x1)) by Th17
.= ((t - a) * (x3 - x1)) - ((s * (x2 - x1)) - (a * (x2 - x1))) by Th9
.= ((t - a) * (x3 - x1)) + (- ((s - a) * (x2 - x1))) by Th16
.= ((t - a) * (x3 - x1)) + ((- (s - a)) * (x2 - x1)) by Th8
.= ((t - a) * (x3 - x1)) + ((a - s) * (x2 - x1)) ;
then t - a = 0 by A1, Def2;
then A15: y3 - x1 = (((1 * x1) + (- (a * x1))) + (a * x3)) - x1 by A10, Th16
.= ((x1 + (- (a * x1))) + (a * x3)) - x1 by EUCLID_4:3
.= (((- (a * x1)) + (a * x3)) + x1) - x1 by RVSUM_1:32
.= ((- (a * x1)) + (a * x3)) + (x1 - x1) by Th10
.= ((- (a * x1)) + (a * x3)) + (0* n) by Th7
.= (- (a * x1)) + (a * x3) by EUCLID_4:1
.= a * (x3 - x1) by Th17 ;
a - s = 0 by A1, A14, Def2;
then A16: y2 - x1 = (((1 * x1) + (- (a * x1))) + (a * x2)) - x1 by A13, Th16
.= ((x1 + (- (a * x1))) + (a * x2)) - x1 by EUCLID_4:3
.= (((- (a * x1)) + (a * x2)) + x1) - x1 by RVSUM_1:32
.= ((- (a * x1)) + (a * x2)) + (x1 - x1) by Th10
.= ((- (a * x1)) + (a * x2)) + (0* n) by Th7
.= (- (a * x1)) + (a * x2) by EUCLID_4:1
.= a * (x2 - x1) by Th17 ;
y3 - y2 <> 0* n by A11, Def1;
hence ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) by A12, A16, A15, EUCLID_4:3; :: thesis: verum

end;

now

assume ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ; :: thesis: ex a being Real ex x2, x3, y2, y3 being Element of REAL n st L1 // L2
then consider a being Real such that
A17: a <> 0 and
A18: y2 - x1 = a * (x2 - x1) and
A19: y3 - x1 = a * (x3 - x1) ;
take a = a; :: thesis: ex x2, x3, y2, y3 being Element of REAL n st L1 // L2
take x2 = x2; :: thesis: ex x3, y2, y3 being Element of REAL n st L1 // L2
take x3 = x3; :: thesis: ex y2, y3 being Element of REAL n st L1 // L2
take y2 = y2; :: thesis: ex y3 being Element of REAL n st L1 // L2
take y3 = y3; :: thesis: L1 // L2
x2 <> x3 by A1, Th42;
then A20: x3 - x2 <> 0* n by Th14;
A21: y3 - y2 = (x1 + (a * (x3 - x1))) - y2 by A19, Th11
.= ((a * (x3 - x1)) + x1) - (x1 + (a * (x2 - x1))) by A18, Th11
.= (((a * (x3 - x1)) + x1) - x1) - (a * (x2 - x1)) by RVSUM_1:60
.= ((a * (x3 - x1)) + (x1 - x1)) - (a * (x2 - x1)) by Th10
.= ((a * (x3 - x1)) + (0* n)) - (a * (x2 - x1)) by Th7
.= (a * (x3 - x1)) - (a * (x2 - x1)) by EUCLID_4:1
.= ((a * x3) + (- (a * x1))) - (a * (x2 - x1)) by Th17
.= ((a * x3) + (- (a * x1))) - ((- (a * x1)) + (a * x2)) by Th17
.= (((a * x3) + (- (a * x1))) - (- (a * x1))) - (a * x2) by RVSUM_1:60
.= ((a * x3) + ((- (a * x1)) - (- (a * x1)))) - (a * x2) by Th10
.= ((a * x3) + (0* n)) - (a * x2) by Th7
.= (a * x3) - (a * x2) by EUCLID_4:1
.= a * (x3 - x2) by Th17 ;
then y3 - y2 <> 0* n by A17, A20, EUCLID_4:5;
then y3 - y2 // x3 - x2 by A21, A20, Def1;
hence L1 // L2 by A4, A5, Def7; :: thesis: verum

end;

hence ( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 ) ; :: thesis: verum