reconsider T = the topology of X as Subset-Family of X ;
take T ; :: thesis: ( T c= the topology of X & the topology of X c= UniCl T )
thus T c= the topology of X ; :: thesis: the topology of X c= UniCl T
now
let A be Subset of X; :: thesis: ( A in the topology of X implies A in UniCl T )
reconsider B = {A} as Subset-Family of X by SUBSET_1:63;
assume A in the topology of X ; :: thesis: A in UniCl T
then A1: B c= T by ZFMISC_1:37;
A = union B by ZFMISC_1:31;
hence A in UniCl T by A1, Def1; :: thesis: verum
end;
hence the topology of X c= UniCl T by SUBSET_1:7; :: thesis: verum