consider SM being op-discrete OrderSortedSign;
take SM ; :: thesis: SM is regular
thus SM is regular by Th12; :: thesis: verum