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:22;

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) ;
set s = the Element of S;
consider n being Node of t such that
the Element of S = t | n and
A4: ( not n in Leaves (dom t) or t . n in C ) by Th17;
A5: dom t = {{}} by A2, TREES_1:29;
then n = {} by TARSKI:def 1;
then e ^ <*0*> in dom t by A3, A4, TREES_1:54;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum