reconsider e' = e as Element of the Sorts of (FreeMSA the Sorts of A) . v ;
reconsider d = depth e' as Element of NAT by ORDINAL1:def 13;
take d ; :: thesis: ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & d = depth e' )
take e' ; :: thesis: ( e = e' & d = depth e' )
thus ( e = e' & d = depth e' ) ; :: thesis: verum