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