let SF be SigmaField of X; :: thesis: ( SF is cap-finite-partition-closed & SF is diff-c=-finite-partition-closed & SF is with_countable_Cover & SF is with_empty_element )
set U = {X};
A1: {X} is Subset-Family of X by ZFMISC_1:68;
A2: union {X} = X ;
X is Element of SF by PROB_1:5;
then {X} is Subset of SF by SUBSET_1:33;
hence ( SF is cap-finite-partition-closed & SF is diff-c=-finite-partition-closed & SF is with_countable_Cover & SF is with_empty_element ) by A1, SETFAM_1:45, SETFAM_1:def 8, A2, SRINGS_1:def 4, PROB_1:4; :: thesis: verum