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 Th16;
then consider n being Node of t2 such that
A1: [{} ,t1] = [n,(t2 | n)] ;
( {} = n & t1 = t2 | n ) by A1, ZFMISC_1:33;
hence t1 = t2 by Th1; :: thesis: verum