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