theorem Th4: :: SCPISORT:4

for s1, s2 being State of SCMPDS st ( for a being Int_position holds s1 . a = s2 . a ) holds
Initialize s1 = Initialize s2