set G = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph;
set F = NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph;
A3: dom (NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph) = NAT by FUNCOP_1:13;
reconsider F = NAT --> the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph as ManySortedSet of NAT ;

now :: thesis: for x being Nat holds F . x is _Graph

let x be Nat; :: thesis: F . x is _Graph
x in NAT by ORDINAL1:def 12;
then F . x in rng F by A3, FUNCT_1:3;
then F . x in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8;
hence F . x is _Graph by TARSKI:def 1; :: thesis: verum

end;

then reconsider F = F as GraphSeq by Def53;
F . (1 + 1) in rng F by A3, FUNCT_1:3;
then F . (1 + 1) in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8;
then A4: F . (1 + 1) = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def 1;
take F ; :: thesis: ( F is halting & F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple )
F . 1 in rng F by A3, FUNCT_1:3;
then F . 1 in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8;
then F . 1 = the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph by TARSKI:def 1;
hence F is halting by A4; :: thesis: ( F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple )

now :: thesis: for x being Nat holds
( F . x is finite & F . x is loopless & not F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple )

let x be Nat; :: thesis: ( F . x is finite & F . x is loopless & not F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple )
x in NAT by ORDINAL1:def 12;
then F . x in rng F by A3, FUNCT_1:3;
then F . x in { the finite loopless non trivial non-multi non-Dmulti simple Dsimple _Graph} by FUNCOP_1:8;
hence ( F . x is finite & F . x is loopless & not F . x is trivial & F . x is non-multi & F . x is non-Dmulti & F . x is simple & F . x is Dsimple ) by TARSKI:def 1; :: thesis: verum

end;

hence ( F is finite & F is loopless & F is non-trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) ; :: thesis: verum