consider S0 being non empty non void ManySortedSign ;
take s = OSSign S0; :: thesis: ( s is discrete & s is op-discrete & s is discernable )
thus ( s is discrete & s is op-discrete ) by Th5; :: thesis: s is discernable
hence s is discernable by Th4; :: thesis: verum