Fin X is cap-closed

proof

let x, y be set ; :: according to FINSUB_1:def 2 :: thesis: ( not x in Fin X or not y in Fin X or x /\ y in Fin X )
assume ( x in Fin X & y in Fin X ) ; :: thesis: x /\ y in Fin X
then A2: ( x is finite & y is finite & x c= X & y c= X ) by FINSUB_1:def 5;
x /\ y c= x by XBOOLE_1:17;
then ( x /\ y is finite & x /\ y c= X ) by A2;
hence x /\ y in Fin X by FINSUB_1:def 5; :: thesis: verum

end;

hence for b₁ being Subset-Family of X st b₁ = Fin X holds
( b₁ is cap-finite-partition-closed & b₁ is diff-c=-finite-partition-closed & not b₁ is with_non-empty_elements ) by FINSUB_1:7, SETFAM_1:def 8; :: thesis: verum