let Y be non empty set ; :: thesis: %I Y '<' %O Y
A1: ERl (%O Y) = nabla Y by Th37
.= [:Y,Y:] ;
A2: ERl (%I Y) c= ERl (%O Y) by A1;
thus %I Y '<' %O Y by A2, Th24; :: thesis: verum