let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P holds
Line x1,x2 c= P
let x1, x2 be Element of REAL n; :: thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P holds
Line x1,x2 c= P
let P be Element of plane_of_REAL n; :: thesis: ( x1 in P & x2 in P implies Line x1,x2 c= P )
P in plane_of_REAL n ;
then A1: ex P9 being Subset of (REAL n) st
( P = P9 & ex y1, y2, y3 being Element of REAL n st P9 = plane y1,y2,y3 ) ;
assume ( x1 in P & x2 in P ) ; :: thesis: Line x1,x2 c= P
hence Line x1,x2 c= P by A1, Th90; :: thesis: verum