let C be set ; :: thesis: for X being non empty constituted-DTrees set holds
( C -Subtrees X is empty iff for t being Element of X holds
( t is root & not t . {} in C ) )
let X be non empty constituted-DTrees set ; :: thesis: ( C -Subtrees X is empty iff for t being Element of X holds
( t is root & not t . {} in C ) )

hereby :: thesis: ( ( for t being Element of X holds
( t is root & not t . {} in C ) ) implies C -Subtrees X is empty )

assume A1: C -Subtrees X is empty ; :: thesis: for t being Element of X holds
( t is root & not t . {} in C )
let t be Element of X; :: thesis: ( t is root & not t . {} in C )
reconsider e = {} as Node of t by TREES_1:22;
A2: not t | e in C -Subtrees X by A1;
then e in Leaves (dom t) ;
hence ( t is root & not t . {} in C ) by A2, Th4; :: thesis: verum

end;

assume A3: for t being Element of X holds
( t is root & not t . {} in C ) ; :: thesis: C -Subtrees X is empty
assume not C -Subtrees X is empty ; :: thesis: contradiction
then reconsider S = C -Subtrees X as non empty Subset of (Subtrees X) ;
set s = the Element of S;
consider t being Element of X, 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 Th24;
reconsider e = {} as Node of t by TREES_1:22;
t is root by A3;
then A5: dom t = {{}} by 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