let p be FinSequence of (Free (S,X)); :: thesis: p is DTree-yielding
let x be object ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: ( not x in proj2 p or x is set )
assume x in rng p ; :: thesis: x is set
hence x is set ; :: thesis: verum