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)

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

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

then reconsider F = { A where A is Subset of (union P) : for D being set st D in P holds
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;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

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