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