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