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