let t be DecoratedTree; :: thesis: Subtrees {t} = Subtrees t

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Subtrees t c= Subtrees {t}

let x be object ; :: thesis: ( x in Subtrees {t} implies x in Subtrees t )
assume x in Subtrees {t} ; :: thesis: x in Subtrees t
then consider u being Element of {t}, p being Node of u such that
A1: x = u | p ;
u = t by TARSKI:def 1;
hence x in Subtrees t by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Subtrees t or x in Subtrees {t} )
assume x in Subtrees t ; :: thesis: x in Subtrees {t}
then ( t in {t} & ex p being Node of t st x = t | p ) by TARSKI:def 1;
hence x in Subtrees {t} ; :: thesis: verum