let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds
( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for A being Element of S holds
( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )
let A be Element of S; :: thesis: ( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )
A1: union ((PARTITIONS A) /\ (Fin S)) = { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } by ThmVAL1;
then A2: union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed Subset-Family of A by ThmVAL0;
union ((PARTITIONS A) /\ (Fin S)) is diff-c=-finite-partition-closed Subset-Family of A by A1, ThmVAL2;
hence ( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements ) by A2, LemPO; :: thesis: verum