theorem Th1: :: RING_EMB:1

for a being non empty set ex b being object st
for x being set holds not [x,b] in a