:: deftheorem defines the_universe_of YELLOW_6:def 1 :
for X being set holds the_universe_of X = Tarski-Class (the_transitive-closure_of X);