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