let t1, t2 be DecoratedTree; :: thesis: ( t1 in Subtrees t2 implies Subtrees t1 c= Subtrees t2 )
assume t1 in Subtrees t2 ; :: thesis: Subtrees t1 c= Subtrees t2
then consider p being Element of dom t2 such that
A1: t1 = t2 | p ;
thus Subtrees t1 c= Subtrees t2 by A1, TREES_9:13; :: thesis: verum