let A be set ; :: thesis: ( A is empty implies A is finite )
assume A1: A is empty ; :: thesis: A is finite
take {} ; :: according to FINSET_1:def 1 :: thesis: ( rng {} = A & dom {} in omega )
thus rng {} = A by A1; :: thesis: dom {} in omega
thus dom {} in omega by ORDINAL1:def 11; :: thesis: verum