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) )
A1: dom (t | p) = (dom t) | p by TREES_2:def 10;
thus ( t | p is root iff p in Leaves (dom t) ) by A1, Th5; :: thesis: verum