set G = the non non-multi non non-Dmulti _Graph;
take F = NAT --> the non non-multi non non-Dmulti _Graph; :: thesis: ( not F is empty & not F is non-Dmulti & not F is non-multi )
set n = the Nat;
F . the Nat = the non non-multi non non-Dmulti _Graph by ORDINAL1:def 12, FUNCOP_1:7;
hence ( not F is empty & not F is non-Dmulti & not F is non-multi ) ; :: thesis: verum