set F = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } ;
set X = union P;
{ A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } c= bool (union P)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } or x in bool (union P) )
assume x in { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } ; :: thesis: x in bool (union P)
then ex A being Subset of (union P) st
( x = A & ( for D being set st D in P holds
ex d being set st A /\ D c= {d} ) ) ;
hence x in bool (union P) ; :: thesis: verum

end;

then reconsider F = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } as Subset-Family of (union P) ;
take TopStruct(# (union P),F #) ; :: thesis: ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } )
thus ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} } ) ; :: thesis: verum