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 not t | e in C -Subtrees t ;
then ( e in Leaves (dom t) & not t . e in C ) ;
hence ( t is root & not t . {} in C ) by Th4; :: thesis: verum

end;

assume A1: ( t is root & 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
A2: ( s = t | n & ( not n in Leaves (dom t) or t . n in C ) ) by Th18;
A3: dom t = {{} } by A1, Def1, TREES_1:56;
then n = {} by TARSKI:def 1;
then ( e ^ <*0 *> in dom t & e ^ <*0 *> = <*0 *> ) by A1, A2, FINSEQ_1:47, TREES_1:91;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum