let T be TopSpace; :: thesis: for K being Subset-Family of T holds
( the topology of T = UniCl K iff K is Basis of T )
let K be Subset-Family of T; :: thesis: ( the topology of T = UniCl K iff K is Basis of T )
thus ( the topology of T = UniCl K implies K is Basis of T ) :: thesis: ( K is Basis of T implies the topology of T = UniCl K )

proof

assume the topology of T = UniCl K ; :: thesis: K is Basis of T
then ( K c= the topology of T & the topology of T c= UniCl K ) by CANTOR_1:1;
hence K is Basis of T by CANTOR_1:def 2, TOPS_2:64; :: thesis: verum

end;

assume A1: K is Basis of T ; :: thesis: the topology of T = UniCl K
then K c= the topology of T by TOPS_2:64;
then A2: UniCl K c= UniCl the topology of T by CANTOR_1:9;
the topology of T c= UniCl K by A1, CANTOR_1:def 2;
hence ( the topology of T c= UniCl K & UniCl K c= the topology of T ) by A2, CANTOR_1:6; :: according to XBOOLE_0:def 10 :: thesis: verum