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 )
A1: K \ {{} } c= K by XBOOLE_1:36;
reconsider K' = K \ {{} } as Subset-Family of T ;

hereby :: thesis: ( K \ {{} } is Basis of T implies K is Basis of T )

assume A2: K is Basis of T ; :: thesis: K \ {{} } is Basis of T
then A3: K c= the topology of T by CANTOR_1:def 2;
A4: the topology of T c= UniCl K by A2, CANTOR_1:def 2;
A5: K \ {{} } c= the topology of T by A1, A3, XBOOLE_1:1;
the topology of T c= UniCl K' by A4, Th2;
hence K \ {{} } is Basis of T by A5, CANTOR_1:def 2; :: thesis: verum

end;

assume A6: K \ {{} } is Basis of T ; :: thesis: K is Basis of T
then A7: K' c= the topology of T by CANTOR_1:def 2;
A8: the topology of T c= UniCl K' by A6, CANTOR_1:def 2;
A9: K c= the topology of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K or x in the topology of T )
assume A10: 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:5; :: thesis: verum

end;

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

then not x in {{} } by TARSKI:def 1;
then x in K' by A10, XBOOLE_0:def 5;
hence x in the topology of T by A7; :: thesis: verum

end;

end;

end;

UniCl K' c= UniCl K by CANTOR_1:9, XBOOLE_1:36;
then the topology of T c= UniCl K by A8, XBOOLE_1:1;
hence K is Basis of T by A9, CANTOR_1:def 2; :: thesis: verum