let n be Element of NAT ; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds
L1 misses L2
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 // L2 & L1 <> L2 implies L1 misses L2 )
assume A1: ( L1 // L2 & L1 <> L2 ) ; :: thesis: L1 misses L2
assume A2: not L1 misses L2 ; :: thesis: contradiction
consider x1, x2, y1, y2 being Element of REAL n such that
A3: ( L1 = Line x1,x2 & L2 = Line y1,y2 & x2 - x1 // y2 - y1 ) by A1, Def7;
consider x being set such that
A4: ( x in L1 & x in L2 ) by A2, XBOOLE_0:3;
reconsider x = x as Element of REAL n by A4;
A5: ( x2 - x1 <> 0* n & y2 - y1 <> 0* n ) by A3, Def1;
then ( x1 <> x2 & y1 <> y2 ) by Th14;
then A6: ( L1 is being_line & L2 is being_line ) by A3, EUCLID_4:def 2;
then consider x0 being Element of REAL n such that
A7: ( x <> x0 & x0 in L1 ) by EUCLID_4:15;
A8: L1 = Line x,x0 by A4, A6, A7, Th35;
consider y0 being Element of REAL n such that
A9: ( x <> y0 & y0 in L2 ) by A6, EUCLID_4:15;
A10: L2 = Line x,y0 by A4, A6, A9, Th35;
A11: ( x0 - x <> 0* n & y0 - x <> 0* n ) by A7, A9, Th14;
consider a being Real such that
A12: x0 - x = a * (x2 - x1) by A3, A4, A7, Th36;
A13: x0 - x // x2 - x1 by A5, A11, A12, Def1;
consider b being Real such that
A14: y0 - x = b * (y2 - y1) by A3, A4, A9, Th36;
A15: y0 - x // y2 - y1 by A5, A11, A14, Def1;
x0 - x // y2 - y1 by A3, A13, Th38;
then A16: x0 - x // y0 - x by A15, Th38;
A17: Line x,x0 c= Line x,y0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Line x,x0 or y in Line x,y0 )
assume y in Line x,x0 ; :: thesis: y in Line x,y0
then consider t being Real such that
A18: y = ((1 - t) * x) + (t * x0) ;
A19: y = ((1 * x) + (- (t * x))) + (t * x0) by A18, Th16
.= (x + (- (t * x))) + (t * x0) by EUCLID_4:3
.= x + ((t * x0) + (- (t * x))) by RVSUM_1:32
.= x + (t * (x0 - x)) by Th17 ;
consider a being Real such that
A20: x0 - x = a * (y0 - x) by A16, Def1;
y = x + ((t * a) * (y0 - x)) by A19, A20, EUCLID_4:4
.= x + (((t * a) * y0) + (- ((t * a) * x))) by Th17
.= (x + (- ((t * a) * x))) + ((t * a) * y0) by RVSUM_1:32
.= ((1 * x) + (- ((t * a) * x))) + ((t * a) * y0) by EUCLID_4:3
.= ((1 - (t * a)) * x) + ((t * a) * y0) by Th16 ;
hence y in Line x,y0 ; :: thesis: verum

end;

Line x,y0 c= Line x,x0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Line x,y0 or y in Line x,x0 )
assume y in Line x,y0 ; :: thesis: y in Line x,x0
then consider t being Real such that
A21: y = ((1 - t) * x) + (t * y0) ;
A22: y = ((1 * x) + (- (t * x))) + (t * y0) by A21, Th16
.= (x + (- (t * x))) + (t * y0) by EUCLID_4:3
.= x + ((t * y0) + (- (t * x))) by RVSUM_1:32
.= x + (t * (y0 - x)) by Th17 ;
consider a being Real such that
A23: y0 - x = a * (x0 - x) by A16, Def1;
y = x + ((t * a) * (x0 - x)) by A22, A23, EUCLID_4:4
.= x + (((t * a) * x0) + (- ((t * a) * x))) by Th17
.= (x + (- ((t * a) * x))) + ((t * a) * x0) by RVSUM_1:32
.= ((1 * x) + (- ((t * a) * x))) + ((t * a) * x0) by EUCLID_4:3
.= ((1 - (t * a)) * x) + ((t * a) * x0) by Th16 ;
hence y in Line x,x0 ; :: thesis: verum

end;

hence contradiction by A1, A8, A10, A17, XBOOLE_0:def 10; :: thesis: verum