let M be subset-closed SubsetFamilyStr; :: thesis: ( not M is void iff {} in the_family_of M )

hereby :: thesis: ( {} in the_family_of M implies not M is void )

assume not M is void ; :: thesis: {} in the_family_of M
then reconsider M' = M as non void subset-closed SubsetFamilyStr ;
consider a being independent Subset of M';
{} c= a by XBOOLE_1:2;
then {} is independent Subset of M' by Th2;
hence {} in the_family_of M by Def8; :: thesis: verum

end;

assume {} in the_family_of M ; :: thesis: not M is void
hence not the topology of M is empty ; :: according to PENCIL_1:def 4 :: thesis: verum