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
A2: ex f being Function st
( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) from NAT_1:sch 11();
thus x in the_transitive-closure_of X by A1, A2, Def7; :: thesis: verum