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

hence not the topology of M is empty ; :: according to PENCIL_1:def 4 :: thesis: verum

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

assume
{} in the_family_of M
; :: thesis: 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;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

hence not the topology of M is empty ; :: according to PENCIL_1:def 4 :: thesis: verum