Trees is constituted-Trees

proof

let x be set ; :: according to TREES_3:def 3 :: thesis: ( x in Trees implies x is Tree )
thus ( x in Trees implies x is Tree ) by Def1; :: thesis: verum

end;

hence Trees is constituted-Trees ; :: thesis: verum