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