A1: dom p <> {} ;
assume x -tree p is root ; :: thesis: contradiction
then A2: dom (x -tree p) = tree {} by TREES_3:55, 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 doms p = {} by A2, TREES_3:53;
hence contradiction by A1, RELAT_1:60, TREES_3:39; :: thesis: verum