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

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