let n be Element of 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 )
assume A1: ( x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 ) ; :: thesis: Line x1,x2 meets Line y1,y2
then ( x2 - x1 <> 0* n & y2 - y1 <> 0* n ) by Lm2;
then A2: ( x2 <> x1 & y2 <> y1 ) by Th14;
reconsider L1 = Line x1,x2, L2 = Line y1,y2 as Element of line_of_REAL n by Th52;
( L1 c= P & L2 c= P ) by A1, Th100;
then A3: L1,L2 are_coplane by Th101;
A4: ( L1 is being_line & L2 is being_line ) by A2, EUCLID_4:def 2;
A5: ( x1 in L1 & x2 in L1 & y1 in L2 & y2 in L2 ) by EUCLID_4:10;
L1 meets L2

proof

assume L1 misses L2 ; :: thesis: contradiction
then L1 // L2 by A3, A4, Th118;
hence contradiction by A1, A2, A5, Lm3, Th82; :: thesis: verum

end;

hence Line x1,x2 meets Line y1,y2 ; :: thesis: verum