thus ( A is finite-membered implies for B being set st B in A holds
B is finite ) :: thesis: ( ( for B being set st B in A holds
B is finite ) implies A is finite-membered )

proof

assume for a being Element of A holds a is finite ; :: according to LEXBFS:def 1 :: thesis: for B being set st B in A holds
B is finite
hence for B being set st B in A holds
B is finite ; :: thesis: verum

end;

assume A1: for B being set st B in A holds
B is finite ; :: thesis: A is finite-membered
let a be Element of A; :: according to LEXBFS:def 1 :: thesis: a is finite
( A <> {} or A = {} ) ;
hence a is finite by A1; :: thesis: verum