for A being non empty Subset of RAT+ st A in RAT+ holds
ex s being Element of RAT+ st
( s in A & ( for r being Element of RAT+ st r in A holds
r <=' s ) )