( a is Element of INT & ObjectKind la = INT ) by Th55, INT_1:def 2;
then reconsider a = a as Element of ObjectKind la ;
la .--> a is PartState of SCM ;
hence la .--> a is PartState of SCM ; :: thesis: verum