theorem Th34: :: COH_SP:35

for a, X being set st a c= X holds
[(id a),a] in TOL X