let T be TopSpace; :: thesis: for K being Subset-Family of T holds
( K is Basis of T iff K \ {{}} is Basis of T )
let K be Subset-Family of T; :: thesis: ( K is Basis of T iff K \ {{}} is Basis of T )
reconsider K9 = K \ {{}} as Subset-Family of T ;
A1: UniCl K9 c= UniCl K by CANTOR_1:9, XBOOLE_1:36;
A2: K \ {{}} c= K by XBOOLE_1:36;
hereby :: thesis: ( K \ {{}} is Basis of T implies K is Basis of T )
assume A3: K is Basis of T ; :: thesis: K \ {{}} is Basis of T
then the topology of T c= UniCl K by CANTOR_1:def 2;
then A4: the topology of T c= UniCl K9 by Th1;
K c= the topology of T by A3, TOPS_2:64;
then K \ {{}} c= the topology of T by A2;
hence K \ {{}} is Basis of T by A4, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum
end;
assume A5: K \ {{}} is Basis of T ; :: thesis: K is Basis of T
then A6: K9 c= the topology of T by TOPS_2:64;
A7: K c= the topology of T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K or x in the topology of T )
assume A8: x in K ; :: thesis: x in the topology of T
per cases ( x = {} or x <> {} ) ;
end;
end;
the topology of T c= UniCl K9 by A5, CANTOR_1:def 2;
then the topology of T c= UniCl K by A1;
hence K is Basis of T by A7, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum