let n be 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 that
A1: L1 // L2 and
A2: L1 <> L2 ; :: thesis: L1 misses L2
assume not L1 misses L2 ; :: thesis: contradiction
then consider x being object such that
A3: x in L1 and
A4: x in L2 by XBOOLE_0:3;
reconsider x = x as Element of REAL n by A3;
consider x1, x2, y1, y2 being Element of REAL n such that
A5: L1 = Line (x1,x2) and
A6: L2 = Line (y1,y2) and
A7: x2 - x1 // y2 - y1 by A1;
A8: x2 - x1 <> 0* n by A7;
then x1 <> x2 by Th9;
then A9: L1 is being_line by A5;
then consider x0 being Element of REAL n such that
A10: x <> x0 and
A11: x0 in L1 by EUCLID_4:14;
A12: x0 - x <> 0* n by A10, Th9;
ex a being Real st x0 - x = a * (x2 - x1) by A5, A3, A11, Th31;
then x0 - x // x2 - x1 by A8, A12;
then A13: x0 - x // y2 - y1 by A7, Th33;
A14: y2 - y1 <> 0* n by A7;
then y1 <> y2 by Th9;
then A15: L2 is being_line by A6;
then consider y0 being Element of REAL n such that
A16: x <> y0 and
A17: y0 in L2 by EUCLID_4:14;
A18: y0 - x <> 0* n by A16, Th9;
ex b being Real st y0 - x = b * (y2 - y1) by A6, A4, A17, Th31;
then y0 - x // y2 - y1 by A14, A18;
then A19: x0 - x // y0 - x by A13, Th33;
A20: Line (x,x0) c= Line (x,y0)
proof
let y be object ; :: 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
A21: y = ((1 - t) * x) + (t * x0) ;
consider a being Real such that
A22: x0 - x = a * (y0 - x) by A19;
y = ((1 * x) + (- (t * x))) + (t * x0) by A21, Th11
.= (x + (- (t * x))) + (t * x0) by EUCLID_4:3
.= x + ((t * x0) + (- (t * x))) by RVSUM_1:15
.= x + (t * (x0 - x)) by Th12 ;
then y = x + ((t * a) * (y0 - x)) by A22, EUCLID_4:4
.= x + (((t * a) * y0) + (- ((t * a) * x))) by Th12
.= (x + (- ((t * a) * x))) + ((t * a) * y0) by RVSUM_1:15
.= ((1 * x) + (- ((t * a) * x))) + ((t * a) * y0) by EUCLID_4:3
.= ((1 - (t * a)) * x) + ((t * a) * y0) by Th11 ;
hence y in Line (x,y0) ; :: thesis: verum
end;
A23: Line (x,y0) c= Line (x,x0)
proof
let y be object ; :: 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
A24: y = ((1 - t) * x) + (t * y0) ;
consider a being Real such that
A25: y0 - x = a * (x0 - x) by A19, Def1;
y = ((1 * x) + (- (t * x))) + (t * y0) by A24, Th11
.= (x + (- (t * x))) + (t * y0) by EUCLID_4:3
.= x + ((t * y0) + (- (t * x))) by RVSUM_1:15
.= x + (t * (y0 - x)) by Th12 ;
then y = x + ((t * a) * (x0 - x)) by A25, EUCLID_4:4
.= x + (((t * a) * x0) + (- ((t * a) * x))) by Th12
.= (x + (- ((t * a) * x))) + ((t * a) * x0) by RVSUM_1:15
.= ((1 * x) + (- ((t * a) * x))) + ((t * a) * x0) by EUCLID_4:3
.= ((1 - (t * a)) * x) + ((t * a) * x0) by Th11 ;
hence y in Line (x,x0) ; :: thesis: verum
end;
A26: L2 = Line (x,y0) by A4, A15, A16, A17, Th30;
L1 = Line (x,x0) by A3, A9, A10, A11, Th30;
hence contradiction by A2, A26, A20, A23, XBOOLE_0:def 10; :: thesis: verum