let X be set ; :: thesis: X c= the_transitive-closure_of X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the_transitive-closure_of X )
assume A1: x in X ; :: thesis: x in the_transitive-closure_of X
consider f being Function such that
W1: dom f = omega and
W2: f . 0 = X and
W3: for n being natural number holds f . (succ n) = H₂(n,f . n) from ORDINAL2:sch 18();
reconsider z = 0 as Element of omega by ORDINAL1:def 13;
x in f . z by A1, W2;
hence x in the_transitive-closure_of X by W1, W2, W3, Def7; :: thesis: verum