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

proof

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

per cases ( x in SCM-Data-Loc or x = IC SCMPDS ) 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 SCMPDS ; :: thesis: contradiction

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

end;

end;

end;

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