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