let A be set ; :: thesis: ( A is empty implies A is finite-membered )
assume A1: A is empty ; :: thesis: A is finite-membered
let B be set ; :: according to FINSET_1:def 6 :: thesis: ( B in A implies B is finite )
thus ( B in A implies B is finite ) by A1; :: thesis: verum