let X be set ; :: thesis: ( X is constituted-DTrees implies X is functional )
assume A1: X is constituted-DTrees ; :: thesis: X is functional
let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in X or x is set )
thus ( not x in X or x is set ) by A1, Def5; :: thesis: verum