let X be set ; :: thesis: for S being Subset of X
for A being Element of S holds union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements
let S be Subset of X; :: thesis: for A being Element of S holds union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements
let A be Element of S; :: thesis: union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements
assume not union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements ; :: thesis: contradiction
then {} in union ((PARTITIONS A) /\ (Fin S)) by SETFAM_1:def 8;
then consider x being set such that
A2: {} in x and
A3: x in (PARTITIONS A) /\ (Fin S) by TARSKI:def 4;
( x in PARTITIONS A & x in Fin S ) by A3, XBOOLE_0:def 4;
then x is a_partition of A by PARTIT1:def 3;
hence contradiction by A2; :: thesis: verum