reconsider F = {{}} as Subset-Family of TS by Th46;
take F ; :: thesis: F is with_proper_subsets
assume TS in F ; :: according to SETFAM_1:def 12 :: thesis: contradiction
hence contradiction by TARSKI:def 1; :: thesis: verum