set S0 = the non empty non void ManySortedSign ;
take s = OSSign the non empty non void ManySortedSign ; :: 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