reconsider q = p | NAT as PartState of S by CARD_3:80, RELAT_1:88;
dom q = (dom p) /\ NAT by RELAT_1:90;
then dom q c= NAT by XBOOLE_1:17;
hence for b₁ being PartState of S st b₁ = ProgramPart p holds
b₁ is NAT -defined by RELAT_1:def 18; :: thesis: verum