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 Def12; :: thesis: verum

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 Def12; :: thesis: verum