:: deftheorem defines KurExSet KURATO_1:def 6 :
KurExSet = (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[;