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