let n be 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)
let x1, x2, y1, y2 be 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 P be Element of plane_of_REAL n; ( 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
; 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
hence
Line (x1,x2) meets Line (y1,y2)
; verum