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