let n be Nat; 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; 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; ( 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 )
; Line (x1,x2) c= P
hence
Line (x1,x2) c= P
by A1, Th85; verum