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:47;
not t | e in C -Subtrees X by A1;
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 A2: 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) ;
consider s being Element of S;
consider t being Element of X, n being Node of t such that
A3: ( s = t | n & ( not n in Leaves (dom t) or t . n in C ) ) by Th25;
reconsider e = {} as Node of t by TREES_1:47;
t is root by A2;
then A4: dom t = {{} } by Def1, TREES_1:56;
then n = {} by TARSKI:def 1;
then ( e ^ <*0 *> in dom t & e ^ <*0 *> = <*0 *> ) by A2, A3, FINSEQ_1:47, TREES_1:91;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum