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