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