let s be State of SCM ; :: thesis: dom (s | NAT ) = NAT
NAT c= dom s by Th28;
hence dom (s | NAT ) = NAT by RELAT_1:91; :: thesis: verum