let t1, t2 be finite DecoratedTree; :: thesis: ( t1 in Subtrees t2 implies height (dom t1) <= height (dom t2) )
assume t1 in Subtrees t2 ; :: thesis: height (dom t1) <= height (dom t2)
then consider p being Element of dom t2 such that
A1: t1 = t2 | p ;
consider r being FinSequence of NAT such that
A2: ( r in dom t1 & len r = height (dom t1) ) by TREES_1:def 12;
dom t1 = (dom t2) | p by A1, TREES_2:def 10;
then p ^ r in dom t2 by A2, TREES_1:def 6;
then len (p ^ r) <= height (dom t2) by TREES_1:def 12;
then ( (len p) + (len r) <= height (dom t2) & len r <= (len p) + (len r) ) by NAT_1:11, FINSEQ_1:22;
hence height (dom t1) <= height (dom t2) by A2, XXREAL_0:2; :: thesis: verum