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 . p = t . p ;
hence t . p is Symbol of ; :: thesis: verum