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 Y in the_transitive-closure_of X ; :: thesis: Y c= the_transitive-closure_of X
then consider f being Function, n being Element of omega such that
A1: Y in f . n and
A2: ( dom f = omega & f . 0 = X ) and
A3: for k being natural number holds f . (succ k) = union (f . k) by Def7;
A4: f . (succ n) = union (f . n) by A3;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in the_transitive-closure_of X )
assume x in Y ; :: thesis: x in the_transitive-closure_of X
then A5: x in union (f . n) by A1, TARSKI:def 4;
reconsider m = succ n as Element of omega by ORDINAL1:def 12;
x in f . m by A4, A5;
hence x in the_transitive-closure_of X by A2, A3, Def7; :: thesis: verum