reconsider Tr = Tr as DecoratedTree of the carrier of s ;
reconsider v = v as Element of dom Tr ;
Tr . v is type of s ;
hence Tr . v is type of s ; :: thesis: verum