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