let t be DecoratedTree; :: thesis: for p being Node of t holds
( t | p is root iff p in Leaves (dom t) )
let p be Node of t; :: thesis: ( t | p is root iff p in Leaves (dom t) )
( ( t | p is root implies dom (t | p) = elementary_tree 0 ) & ( dom (t | p) = elementary_tree 0 implies t | p is root ) & dom (t | p) = (dom t) | p & ( p in Leaves (dom t) implies (dom t) | p = elementary_tree 0 ) & ( (dom t) | p = elementary_tree 0 implies p in Leaves (dom t) ) ) by Def1, Th5, TREES_2:def 11;
hence ( t | p is root iff p in Leaves (dom t) ) ; :: thesis: verum