theorem Th1: :: WELLORD2:7

for X, Y being set st Y c= X holds
(RelIncl X) |_2 Y = RelIncl Y