let t be DecoratedTree; :: thesis: for C being set holds
( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )
let C be set ; :: thesis: ( C -Subtrees t is empty iff ( t is root & not t . {} in C ) )
reconsider e = {} as Node of t by TREES_1:47;

hereby :: thesis: ( t is root & not t . {} in C implies C -Subtrees t is empty )

assume C -Subtrees t is empty ; :: thesis: ( t is root & not t . {} in C )
then A1: not t | e in C -Subtrees t ;
then e in Leaves (dom t) ;
hence ( t is root & not t . {} in C ) by A1, Th4; :: thesis: verum

end;

assume that
A2: t is root and
A3: not t . {} in C ; :: thesis: C -Subtrees t is empty
assume not C -Subtrees t is empty ; :: thesis: contradiction
then reconsider S = C -Subtrees t as non empty Subset of (Subtrees t) ;
consider s being Element of S;
consider n being Node of t such that
s = t | n and
A4: ( not n in Leaves (dom t) or t . n in C ) by Th18;
A5: dom t = {{} } by A2, Def1, TREES_1:56;
then n = {} by TARSKI:def 1;
then e ^ <*0 *> in dom t by A3, A4, TREES_1:91;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum