assume x -tree p is root ; :: thesis: contradiction
then A1: dom (x -tree p) = tree {} by TREES_3:52, TREES_9:def 1;
ex q being DTree-yielding FinSequence st
( p = q & dom (x -tree p) = tree (doms q) ) by TREES_4:def 4;
then ( dom p <> {} & doms p = {} ) by A1, TREES_3:50;
hence contradiction by TREES_3:37; :: thesis: verum