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