set F = NAT --> {};
take NAT --> {} ; :: thesis: ( NAT --> {} is finite-yielding & NAT --> {} is natsubset-yielding )
for x being set st x in rng (NAT --> {}) holds
x is finite ;
hence NAT --> {} is finite-yielding by Lm5; :: thesis: NAT --> {} is natsubset-yielding

now

let x be set ; :: thesis: ( x in rng (NAT --> {}) implies x in bool NAT )
assume x in rng (NAT --> {}) ; :: thesis: x in bool NAT
then x = {} by TARSKI:def 1;
then x c= NAT by XBOOLE_1:2;
hence x in bool NAT ; :: thesis: verum

end;

then rng (NAT --> {}) c= bool NAT by TARSKI:def 3;
hence NAT --> {} is natsubset-yielding by Def3; :: thesis: verum