let t be DecoratedTree; :: thesis: ( t is root iff {} in Leaves (dom t) )
reconsider e = {} as Node of t by TREES_1:47;

hereby :: thesis: ( {} in Leaves (dom t) implies t is root )

assume t is root ; :: thesis: {} in Leaves (dom t)
then dom t = elementary_tree 0 by Def1;
then not e ^ <*0 *> in dom t by TARSKI:def 1, TREES_1:56;
hence {} in Leaves (dom t) by TREES_1:91; :: thesis: verum

end;

assume A1: {} in Leaves (dom t) ; :: thesis: t is root
let p be FinSequence of NAT ; :: according to TREES_2:def 1,TREES_9:def 1 :: thesis: ( ( not p in dom t or p in elementary_tree 0 ) & ( not p in elementary_tree 0 or p in dom t ) )

hereby :: thesis: ( not p in elementary_tree 0 or p in dom t )

assume A2: ( p in dom t & not p in elementary_tree 0 ) ; :: thesis: contradiction
then p <> {} by TARSKI:def 1, TREES_1:56;
then consider q being FinSequence of NAT , n being Nat such that
A3: p = <*n*> ^ q by FINSEQ_2:150;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
( <*n*> in dom t & e ^ <*n*> = <*n*> ) by A2, A3, FINSEQ_1:47, TREES_1:46;
hence contradiction by A1, TREES_1:92; :: thesis: verum

end;

assume p in elementary_tree 0 ; :: thesis: p in dom t
then p = {} by TARSKI:def 1, TREES_1:56;
hence p in dom t by TREES_1:47; :: thesis: verum