set G = the _Graph;
set F = NAT --> the _Graph;
reconsider F = NAT --> the _Graph as ManySortedSet of NAT ;
take F ; :: thesis: F is Graph-yielding
thus F is Graph-yielding ; :: thesis: verum