:: deftheorem defines (#INT,<=#) AOFA_A01:def 18 :
(#INT,<=#) = RealPoset INT;