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 ;
TARSKI:def 3 ( 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) }
;
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)
;
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)
; verum