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 b1 being Subset-Family of X st b1 = Fin X holds
( b1 is cap-finite-partition-closed & b1 is diff-c=-finite-partition-closed & not b1 is with_non-empty_elements ) by FINSUB_1:7, SETFAM_1:def 8; :: thesis: verum