for s being Element of RAT+ st s <=' {} holds
s = {} by Th63;