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