theorem :: PARTIT1:35

for Y being non empty set holds %I Y '<' %O Y