for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for v being SortSymbol of S
for n being Nat st 1 <= n holds
( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st
( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )