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
hence ( K c= the topology of T & the topology of T c= UniCl K ) by CANTOR_1:1; :: according to CANTOR_1:def 2 :: thesis: verum

end;

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