set G = the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph;
set F = NAT --> the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph;
reconsider F = NAT --> the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph as ManySortedSet of NAT ;
reconsider F = F as GraphSeq ;
A2: F . (1 + 1) = the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph ;
take F ; :: thesis: ( F is halting & F is _finite & F is loopless & F is _trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple )
F . 1 = the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph ;
hence F is halting by A2; :: thesis: ( F is _finite & F is loopless & F is _trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple )
thus ( F is _finite & F is loopless & F is _trivial & F is non-multi & F is non-Dmulti & F is simple & F is Dsimple ) ; :: thesis: verum