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 <> {} ) ;

suppose x = {} ; :: thesis: x in the topology of T

hence x in the topology of T by PRE_TOPC:1; :: thesis: verum

end;

suppose x <> {} ; :: thesis: x in the topology of T

then not x in {{}} by TARSKI:def 1;
then x in K9 by A8, XBOOLE_0:def 5;
hence x in the topology of T by A6; :: thesis: verum

end;

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