reconsider t = t as Element of TS (DTConMSA V) ;
reconsider t = t as DecoratedTree of the carrier of (DTConMSA V) ;
reconsider p = p as Node of t ;
t . p = t . p ;
hence t . p is Symbol of (DTConMSA V) ; :: thesis: verum