for
y
being
object
st
y
in
f
"
x
holds
y
in
NAT
by
TARSKI:def 3
;
hence
f
"
x
is
Subset
of
NAT
by
TARSKI:def 3
;
:: thesis:
verum