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 A3: x in the_transitive-closure_of X ; :: thesis: x in Y
consider f being Function, n being Element of NAT such that
A4: x in f . n and
dom f = NAT and
A5: f . 0 = X and
A6: for k being Nat holds f . (k + 1) = union (f . k) by A3, Def7;
defpred S₁[ Element of NAT ] means f . $1 c= Y;
A7: S₁[ 0 ] by A1, A5;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: f . k c= Y ; :: thesis: S₁[k + 1]
A10: union (f . k) c= union Y by A9, ZFMISC_1:95;
A11: ( f . (k + 1) = union (f . k) & union Y c= Y ) by A2, A6, Th54;
thus S₁[k + 1] by A10, A11, XBOOLE_1:1; :: thesis: verum

end;

A12: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A8);
A13: f . n c= Y by A12;
thus x in Y by A4, A13; :: thesis: verum