let Y be Subset of X; :: thesis: Y is constituted-Trees
let x be set ; :: according to TREES_3:def 3 :: thesis: ( x in Y implies x is Tree )
thus ( x in Y implies x is Tree ) by Def3; :: thesis: verum