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