let TS be non empty set ; :: thesis: for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets
let A, B be with_proper_subsets Subset-Family of TS; :: thesis: A \/ B is with_proper_subsets
assume TS in A \/ B ; :: according to SETFAM_1:def 12 :: thesis: contradiction
then ( TS in A or TS in B ) by XBOOLE_0:def 3;
hence contradiction by Def13; :: thesis: verum