theorem Th4: :: OSALG_1:4

for S being non empty non void OverloadedMSSign st S is op-discrete holds
S is discernable by Th3;