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

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