:: deftheorem Def1 defines order-sorted OSALG_1:def 1 :
for S being OverloadedRSSign holds
( S is order-sorted iff ( S is reflexive & S is transitive & S is antisymmetric ) );