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