let X be non empty set ; :: thesis: ( X is cap-finite-closed implies X is cap-closed )
assume A1: X is cap-finite-closed ; :: thesis: X is cap-closed
now :: thesis: for a, b being set st a in X & b in X holds
a /\ b in X
let a, b be set ; :: thesis: ( a in X & b in X implies a /\ b in X )
assume ( a in X & b in X ) ; :: thesis: a /\ b in X
then {a,b} c= X by TARSKI:def 2;
then meet {a,b} in X by A1;
hence a /\ b in X by SETFAM_1:11; :: thesis: verum
end;
hence X is cap-closed ; :: thesis: verum