let n be Nat; :: thesis: for x1, x2, y1, y2 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds
Line (x1,x2) meets Line (y1,y2)
let x1, x2, y1, y2 be Element of REAL n; :: thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds
Line (x1,x2) meets Line (y1,y2)
let P be Element of plane_of_REAL n; :: thesis: ( x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 implies Line (x1,x2) meets Line (y1,y2) )
reconsider L1 = Line (x1,x2), L2 = Line (y1,y2) as Element of line_of_REAL n by Th47;
assume that
A1: ( x1 in P & x2 in P & y1 in P & y2 in P ) and
A2: x2 - x1,y2 - y1 are_lindependent2 ; :: thesis: Line (x1,x2) meets Line (y1,y2)
A3: ( x1 in L1 & x2 in L1 ) by EUCLID_4:9;
( L1 c= P & L2 c= P ) by A1, Th95;
then A4: L1,L2 are_coplane by Th96;
A5: ( y1 in L2 & y2 in L2 ) by EUCLID_4:9;
y2 - y1 <> 0* n by A2, Lm2;
then A6: y2 <> y1 by Th9;
then A7: L2 is being_line ;
x2 - x1 <> 0* n by A2, Lm2;
then A8: x2 <> x1 by Th9;
then A9: L1 is being_line ;
L1 meets L2
proof
assume L1 misses L2 ; :: thesis: contradiction
then L1 // L2 by A4, A9, A7, Th113;
hence contradiction by A2, A8, A6, A3, A5, Lm3, Th77; :: thesis: verum
end;
hence Line (x1,x2) meets Line (y1,y2) ; :: thesis: verum