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