:: deftheorem Def1 defines Trees TREES_3:def 1 :
for b₁ being set holds
( b₁ = Trees iff for x being object holds
( x in b₁ iff x is Tree ) );