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

now :: thesis: for C being object st C in { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } holds

C in bool the carrier of X

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
by TARSKI:def 3; :: thesis: verumC in bool the carrier of X

let C be object ; :: 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;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