theorem Th2: :: SCMPDS_2:5

for l being Int_position holds Values l = INT