let X be set ; :: thesis: the_transitive-closure_of X is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in the_transitive-closure_of X or Y c= the_transitive-closure_of X )
assume A1: Y in the_transitive-closure_of X ; :: thesis: Y c= the_transitive-closure_of X
consider f being Function, n being Element of NAT such that
A2: Y in f . n and
A3: ( dom f = NAT & f . 0 = X ) and
A4: for k being Nat holds f . (k + 1) = union (f . k) by A1, Def7;
A5: f . (n + 1) = union (f . n) by A4;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in the_transitive-closure_of X )
assume A6: x in Y ; :: thesis: x in the_transitive-closure_of X
A7: x in union (f . n) by A2, A6, TARSKI:def 4;
thus x in the_transitive-closure_of X by A3, A4, A5, A7, Def7; :: thesis: verum