set R = the_transitive-closure_of {X};
take T = Tarski-Class (the_transitive-closure_of {X}); :: thesis: X in T
A1: union T c= T by CLASSES1:48;
( X in {X} & {X} c= the_transitive-closure_of {X} ) by CLASSES1:52, TARSKI:def 1;
then ( X in the_transitive-closure_of {X} & the_transitive-closure_of {X} in T ) by CLASSES1:2;
then X in union T by TARSKI:def 4;
hence X in T by A1; :: thesis: verum