let X be set ; :: thesis: X c= the_transitive-closure_of X
let x be object ; :: 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
A2: dom f = omega and
A3: f . 0 = X and
A4: for n being Nat holds f . (succ n) = H₂(n,f . n) from ORDINAL2:sch 18();
reconsider z = 0 as Element of omega by ORDINAL1:def 12;
x in f . z by A1, A3;
hence x in the_transitive-closure_of X by A2, A3, A4, Def7; :: thesis: verum