theorem Th5: :: OSALG_1:5
for S0 being non empty non void ManySortedSign holds
( OSSign S0 is discrete & OSSign S0 is op-discrete )