set FF = { F where F is Subset of FT : ( A c= F & F is open ) } ;
{ F where F is Subset of FT : ( A c= F & F is open ) } c= bool the carrier of FT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Subset of FT : ( A c= F & F is open ) } or x in bool the carrier of FT )
assume x in { F where F is Subset of FT : ( A c= F & F is open ) } ; :: thesis: x in bool the carrier of FT
then ex F being Subset of FT st
( x = F & A c= F & F is open ) ;
hence x in bool the carrier of FT ; :: thesis: verum

end;

then reconsider FF = { F where F is Subset of FT : ( A c= F & F is open ) } as Subset-Family of FT ;
union FF is Subset of FT ;
hence union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT ; :: thesis: verum