( a is Element of INT & ObjectKind la = INT ) by INT_1:def 2, SCMPDS_2:13;
hence la .--> a is FinPartState of SCMPDS by AMI_1:59; :: thesis: verum