let t1, t2 be DecoratedTree; :: thesis: ( FixedSubtrees t1 = FixedSubtrees t2 implies t1 = t2 )
assume FixedSubtrees t1 = FixedSubtrees t2 ; :: thesis: t1 = t2
then [{},t1] in FixedSubtrees t2 by Th15;
then consider n being Node of t2 such that
A1: [{},t1] = [n,(t2 | n)] ;
( {} = n & t1 = t2 | n ) by A1, XTUPLE_0:1;
hence t1 = t2 by Th1; :: thesis: verum