:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def 7 :
for X, b₂ being set holds
( b₂ = the_transitive-closure_of X iff for x being object holds
( x in b₂ iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) );