reconsider z = {} as FinPartState of S by CARD_3:66;
take z ; :: thesis: z is programmed
thus dom z c= IL by RELAT_1:60, XBOOLE_1:2; :: according to AMI_1:def 40 :: thesis: verum