let t be DecoratedTree; :: thesis: for C being set holds C -Subtrees {t} = C -Subtrees t
let C be set ; :: thesis: C -Subtrees {t} = C -Subtrees t

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

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

end;

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