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
A2: Y in f . n and
A3: ( dom f = omega & f . 0 = X ) and
A4: for k being natural number holds f . (succ k) = union (f . k) by Def7;
A5: f . (succ n) = 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 x in Y ; :: thesis: x in the_transitive-closure_of X
then A7: x in union (f . n) by A2, TARSKI:def 4;
reconsider m = succ n as Element of omega by ORDINAL1:def 13;
x in f . m by A5, A7;
hence x in the_transitive-closure_of X by A3, A4, Def7; :: thesis: verum