let X, Y be set ; :: thesis: ( X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y )
assume that
A1: X c= Y and
A2: Y is epsilon-transitive ; :: thesis: the_transitive-closure_of X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the_transitive-closure_of X or x in Y )
assume x in the_transitive-closure_of X ; :: thesis: x in Y
then consider f being Function, n being Element of omega such that
A4: x in f . n and
dom f = omega and
A5: f . 0 = X and
A6: for k being natural number holds f . (succ k) = union (f . k) by Def7;
defpred S₁[ natural number ] means f . $1 c= Y;
A7: S₁[ 0 ] by A1, A5;
A8: for k being natural number st S₁[k] holds
S₁[ succ k]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[ succ k] )
assume f . k c= Y ; :: thesis: S₁[ succ k]
then A10: union (f . k) c= union Y by ZFMISC_1:95;
( f . (succ k) = union (f . k) & union Y c= Y ) by A2, A6, Th54;
hence S₁[ succ k] by A10, XBOOLE_1:1; :: thesis: verum

end;

S₁[n] from ORDINAL2:sch 17(A7, A8);
then f . n c= Y ;
hence x in Y by A4; :: thesis: verum