thus ( X is finite-character implies for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) ) :: thesis: ( ( for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) ) implies X is finite-character )

proof

assume A1: X is finite-character ; :: thesis: for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X )
let Y be set ; :: thesis: ( Y in X iff for S being finite Subset of Y holds S in X )
thus ( Y in X implies for S being finite Subset of Y holds S in X ) :: thesis: ( ( for S being finite Subset of Y holds S in X ) implies Y in X )

proof

assume Y in X ; :: thesis: for S being finite Subset of Y holds S in X
then consider B being set such that
A3: ( B = Y & ( for S being finite Subset of B holds S in X ) ) by A1;
thus for S being finite Subset of Y holds S in X by A3; :: thesis: verum

end;

thus ( ( for S being finite Subset of Y holds S in X ) implies Y in X ) by A1; :: thesis: verum

end;

assume A11: for Y being set holds
( Y in X iff for S being finite Subset of Y holds S in X ) ; :: thesis: X is finite-character
let a be object ; :: according to PROOFS_1:def 27 :: thesis: ( a in X iff ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) )
thus ( a in X implies ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) ) :: thesis: ( ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) ) implies a in X )

proof

assume A12: a in X ; :: thesis: ex B being set st
( B = a & ( for S being finite Subset of B holds S in X ) )
then reconsider B = a as set ;
take B ; :: thesis: ( B = a & ( for S being finite Subset of B holds S in X ) )
thus ( B = a & ( for S being finite Subset of B holds S in X ) ) by A11, A12; :: thesis: verum

end;

given B being set such that A20: ( B = a & ( for S being finite Subset of B holds S in X ) ) ; :: thesis: a in X
thus a in X by A11, A20; :: thesis: verum