for n being Nat
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)