set q = p \ (ProgramPart p);
dom p c= the carrier of S by RELAT_1:def 18;
then p \ (ProgramPart p) = p | (the carrier of S \ NAT ) by RELAT_1:211;
thus p \ (ProgramPart p) is PartState of S ; :: thesis: verum