set A = { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ;
{ P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } c= bool (REAL n)
proof
let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } or P in bool (REAL n) )
assume P in { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ; :: thesis: P in bool (REAL n)
then ex P9 being Subset of (REAL n) st
( P = P9 & ex x1, x2, x3 being Element of REAL n st P9 = plane (x1,x2,x3) ) ;
hence P in bool (REAL n) ; :: thesis: verum
end;
hence { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } is Subset-Family of (REAL n) ; :: thesis: verum