let x be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in rng (roots p) or x in D )
assume x in rng (roots p) ; :: thesis: x in D
then consider k being object such that
A1: k in dom (roots p) and
A2: x = (roots p) . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A1;
A3: dom (roots p) = dom p by TREES_3:def 18;
then consider t being DecoratedTree such that
A4: t = p . k and
A5: (roots p) . k = t . {} by A1, TREES_3:def 18;
reconsider t = t as DecoratedTree of D by A1, A3, A4, Th2, TREES_3:def 6;
reconsider r = {} as Node of t by TREES_1:22;
t . r in D ;
hence x in D by A2, A5; :: thesis: verum