let s1, s2 be State of SCMPDS; :: thesis: ( s1,s2 equal_outside NAT iff s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) )
set Y = NAT ;
set X = SCM-Data-Loc \/ {(IC )};
A1: (((SCM-Data-Loc \/ {(IC )}) \/ NAT) \ NAT) \/ NAT = ((SCM-Data-Loc \/ {(IC )}) \/ NAT) \/ NAT by XBOOLE_1:39
.= (SCM-Data-Loc \/ {(IC )}) \/ (NAT \/ NAT) by XBOOLE_1:4
.= NAT \/ (SCM-Data-Loc \/ {(IC )}) ;
A2: NAT misses ((SCM-Data-Loc \/ {(IC )}) \/ NAT) \ NAT by XBOOLE_1:79;
A3: SCM-Data-Loc \/ {(IC )} misses NAT

proof

assume SCM-Data-Loc \/ {(IC )} meets NAT ; :: thesis: contradiction
then consider x being set such that
A4: x in SCM-Data-Loc \/ {(IC )} and
A5: x in NAT by XBOOLE_0:3;
A6: ( x in SCM-Data-Loc or x in {(IC )} ) by A4, XBOOLE_0:def 3;

per cases ( x in SCM-Data-Loc or x = IC ) by A6, TARSKI:def 1;

suppose x in SCM-Data-Loc ; :: thesis: contradiction

hence contradiction by A5, AMI_2:29, XBOOLE_0:3; :: thesis: verum

end;

suppose x = IC ; :: thesis: contradiction

then reconsider l = IC as Element of NAT by A5;
l = IC ;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

dom s2 = the carrier of SCMPDS by PARTFUN1:def 4;
then dom s2 = (SCM-Data-Loc \/ {(IC )}) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then A7: (dom s2) \ NAT = SCM-Data-Loc \/ {(IC )} by A1, A2, A3, XBOOLE_1:72;
dom s1 = the carrier of SCMPDS by PARTFUN1:def 4;
then dom s1 = (SCM-Data-Loc \/ {(IC )}) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then (dom s1) \ NAT = SCM-Data-Loc \/ {(IC )} by A1, A2, A3, XBOOLE_1:72;
hence ( s1,s2 equal_outside NAT iff s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) ) by A7, FUNCT_7:def 2; :: thesis: verum