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 NAT such that
A1: Y in f . n and
A2: ( dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) by Def7;
A3: f . (n + 1) = union (f . n) by A2;
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 x in union (f . n) by A1, TARSKI:def 4;
hence x in the_transitive-closure_of X by A2, A3, Def7; :: thesis: verum