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

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