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
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;
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: verum