set FF = { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;
{ (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } c= bool the carrier of X

proof

now

let C be set ; :: thesis: ( C in { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } implies C in bool the carrier of X )
assume C in { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ; :: thesis: C in bool the carrier of X
then ex P, S being Subset of X st
( C = P \/ (S /\ A) & P in the topology of X & S in the topology of X ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

hence { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } c= bool the carrier of X by TARSKI:def 3; :: thesis: verum

end;

hence { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } is Subset-Family of X ; :: thesis: verum