theorem Th7: :: CLASSES2:7

for X, W being set st W is subset-closed & X is epsilon-transitive & X in W holds
X c= W ;