let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P holds
plane (x1,x2,x3) c= P
let x1, x2, x3 be Element of REAL n; :: thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P holds
plane (x1,x2,x3) c= P
let P be Element of plane_of_REAL n; :: thesis: ( x1 in P & x2 in P & x3 in P implies plane (x1,x2,x3) 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 & x3 in P ) ; :: thesis: plane (x1,x2,x3) c= P
hence plane (x1,x2,x3) c= P by A1, Th83; :: thesis: verum