for G being non empty 1-sorted holds ((SCM-VAL G) * SCM-OK) . NAT = NAT