set SM = the op-discrete OrderSortedSign;
take the op-discrete OrderSortedSign ; :: thesis: the op-discrete OrderSortedSign is regular
thus the op-discrete OrderSortedSign is regular by Th12; :: thesis: verum