let s1, s2 be State of SCMPDS ; :: thesis: ( s1,s2 equal_outside NAT implies DataPart s1 = DataPart s2 )
assume s1,s2 equal_outside NAT ; :: thesis: DataPart s1 = DataPart s2
then for a being Int_position holds s1 . a = s2 . a by Th13;
hence DataPart s1 = DataPart s2 by Th23; :: thesis: verum