let W, X be set ; :: thesis: ( W is subset-closed & X is epsilon-transitive & X in W implies X c= W )
assume that
A1: for X, Y being set st X in W & Y c= X holds
Y in W and
A2: for Y being set st Y in X holds
Y c= X and
A3: X in W ; :: according to ORDINAL1:def 2,CLASSES1:def 1 :: thesis: X c= W
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in W )
thus ( not x in X or x in W ) by A1, A2, A3; :: thesis: verum