let n be 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, Th85; :: thesis: verum