let GS be GraphSeq; :: thesis: ( GS is loopless & GS is non-multi implies GS is simple )
assume ( GS is loopless & GS is non-multi ) ; :: thesis: GS is simple
then reconsider GS9 = GS as loopless non-multi GraphSeq ;
for x being Nat holds GS9 . x is simple ;
hence GS is simple by Def66; :: thesis: verum