let X, Y be set ; :: thesis: ( X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y )
assume A1: ( X c= Y & 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 NAT such that
A2: ( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) by Def7;
defpred S₁[ Element of NAT ] means f . $1 c= Y;
A3: S₁[ 0 ] by A1, A2;
A4: 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 f . k c= Y ; :: thesis: S₁[k + 1]
then ( union (f . k) c= union Y & f . (k + 1) = union (f . k) & f . (k + 1) = f . (k + 1) & union Y c= Y ) by A1, A2, Th54, ZFMISC_1:95;
hence S₁[k + 1] by XBOOLE_1:1; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
then ( f . n = f . n & f . n c= Y ) ;
hence x in Y by A2; :: thesis: verum