hereby :: thesis: ( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 )
thus
( ( for r being Element of RAT+ holds not for s being Element of RAT+ holds ( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 )
; :: thesis: verum