let s1, s2 be State of SCMPDS; :: thesis: ( s1,s2 equal_outside NAT iff ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) )
thus ( s1,s2 equal_outside NAT implies ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) ) by COMPOS_1:24, COMPOS_1:138; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies s1,s2 equal_outside NAT )
assume that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 ; :: thesis: s1,s2 equal_outside NAT
for a being Int_position holds s1 . a = s2 . a by A2, SCMPDS_4:23;
hence s1,s2 equal_outside NAT by A1, SCMPDS_4:11; :: thesis: verum