let t be DecoratedTree; :: thesis: ( t is root iff {} in Leaves (dom t) )
reconsider e = {} as Node of t by TREES_1:22;
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 ;
then not e ^ <*0*> in dom t by TARSKI:def 1, TREES_1:29;
hence {} in Leaves (dom t) by TREES_1:54; :: 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 that
A2: p in dom t and
A3: not p in elementary_tree 0 ; :: thesis: contradiction
p <> {} by A3, TARSKI:def 1, TREES_1:29;
then consider q being FinSequence of NAT , n being Element of NAT such that
A4: p = <*n*> ^ q by FINSEQ_2:130;
A5: e ^ <*n*> = <*n*> by FINSEQ_1:34;
<*n*> in dom t by A2, A4, TREES_1:21;
hence contradiction by A1, A5, TREES_1:55; :: thesis: verum
end;
assume p in elementary_tree 0 ; :: thesis: p in dom t
then p = {} by TARSKI:def 1, TREES_1:29;
hence p in dom t by TREES_1:22; :: thesis: verum