s . NAT in pi ((product ((SCM-VAL G) * SCM-OK)),NAT) by CARD_3:def 6;
hence s . NAT is Element of NAT by Th4; :: thesis: verum