:: deftheorem defines op-discrete OSALG_1:def 4 :
for S being non empty non void OverloadedMSSign holds
( S is op-discrete iff the Overloading of S = id the carrier' of S );