:: deftheorem defines SCM-VAL SCMRING1:def 3 :
for S being non empty 1-sorted holds SCM-VAL S = <%NAT, the carrier of S%>;