let F be Relation; :: thesis: ( F is empty implies F is finite-yielding )
assume A1: F is empty ; :: thesis: F is finite-yielding
let x be set ; :: according to FINSET_1:def 2 :: thesis: ( x in rng F implies x is finite )
thus ( x in rng F implies x is finite ) by A1; :: thesis: verum