let X be non empty set ; :: thesis: for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)
let Y be Subset-Family of X; :: thesis: Y is Basis of TopStruct(# X,(UniCl Y) #)
Y c= UniCl Y by Th1;
hence Y is Basis of TopStruct(# X,(UniCl Y) #) by Def2; :: thesis: verum