theorem :: TREES_3:1

for X being set holds
( X is constituted-Trees iff X c= Trees )