let n be Element of NAT ; 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); 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) ) }
XBOOLE_0:def 10 { 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
object ;
TARSKI:def 3 ( 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)
;
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, Th48;
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) ) }
;
verum
end;
let x be object ; TARSKI:def 3 ( 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) ) }
; 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 Th52; verum