let n be Element of NAT ; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: plane (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
thus plane (p1,p2,p3) c= { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } c= plane (p1,p2,p3)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in plane (p1,p2,p3) or x in { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } )
assume A1: x in plane (p1,p2,p3) ; :: thesis: x in { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
then reconsider p0 = x as Point of (TOP-REAL n) ;
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A1, Th57;
hence x in { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } or x in plane (p1,p2,p3) )
assume x in { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ; :: thesis: x in plane (p1,p2,p3)
then ex p being Point of (TOP-REAL n) st
( p = x & ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ;
hence x in plane (p1,p2,p3) by Th61; :: thesis: verum