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 object ; :: 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
A3: x in f . n and
dom f = omega and
A4: f . 0 = X and
A5: for k being Nat holds f . (succ k) = union (f . k) by Def7;
defpred S₁[ Nat] means f . $1 c= Y;
A6: S₁[ 0 ] by A1, A4;
A7: for k being Nat st S₁[k] holds
S₁[ succ k]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[ succ k] )
assume f . k c= Y ; :: thesis: S₁[ succ k]
then A8: union (f . k) c= union Y by ZFMISC_1:77;
( f . (succ k) = union (f . k) & union Y c= Y ) by A2, A5, Th48;
hence S₁[ succ k] by A8, XBOOLE_1:1; :: thesis: verum

end;

S₁[n] from ORDINAL2:sch 17(A6, A7);
hence x in Y by A3; :: thesis: verum