defpred S₁[ set ] means ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & $1 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) );
{ p where p is Point of (TOP-REAL n) : S₁[p] } is Subset of (TOP-REAL n) from DOMAIN_1:sch 7();
hence { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } is Subset of (TOP-REAL n) ; :: thesis: verum