theorem Th8: :: ORDINAL6:8

for X, x, y being set st [x,y] in RelIncl X holds
x c= y