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 M9 = M as non void subset-closed SubsetFamilyStr ;
set a = the independent Subset of M9;
{} c= the independent Subset of M9 ;
then {} is independent Subset of M9 by Th1;
hence {} in the_family_of M by Def2; :: 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