let X be set ; :: thesis: ( X is epsilon-transitive & X is power-closed implies X is subset-closed )
assume A1: ( X is epsilon-transitive & X is power-closed ) ; :: thesis: X is subset-closed
let A, B be set ; :: according to CLASSES1:def 1 :: thesis: ( not A in X or not B c= A or B in X )
assume A2: ( A in X & B c= A ) ; :: thesis: B in X
( B in bool A & bool A c= X ) by A1, A2;
hence B in X ; :: thesis: verum