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