( ObjectKind la = the Instructions of SCMPDS & ObjectKind lb = the Instructions of SCMPDS ) by AMI_1:def 14;
hence la,lb --> a,b is FinPartState of by AMI_1:58; :: thesis: verum