let a be Element of A0,s; :: thesis: a is DecoratedTree-like
a is Element of the Sorts of A0 . s ;
hence a is DecoratedTree-like ; :: thesis: verum