theorem Th1: :: ORDINAL1:5

for X, Y being set st Y in X holds
not X c= Y