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 Nat holds f . (succ k) = union (f . k) by Def7;
let x be object ; :: 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 A4: 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 A3, A4;
hence x in the_transitive-closure_of X by A2, A3, Def7; :: thesis: verum