let P be a_partition of X; :: thesis: P is with_non-empty_elements

assume {} in P ; :: according to SETFAM_1:def 8 :: thesis: contradiction

hence contradiction by Def4; :: thesis: verum

assume {} in P ; :: according to SETFAM_1:def 8 :: thesis: contradiction

hence contradiction by Def4; :: thesis: verum