let T be TopSpace; 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; ( 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 )
by CANTOR_1:1, CANTOR_1:def 2, TOPS_2:64; ( K is Basis of T implies the topology of T = UniCl K )
assume A1:
K is Basis of T
; 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; XBOOLE_0:def 10 verum