let S be TopStruct ; :: thesis: the topology of S is Basis of S
the topology of S c= UniCl the topology of S by Th1;
hence the topology of S is Basis of S by Def2; :: thesis: verum