let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds
s1 = s2
let s1, s2 be State of S; :: thesis: ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 )
s1 = s1 | ((Data-Locations ) \/ {(IC )}) by LmAA;
hence ( s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) implies s1 = s2 ) by LmAA; :: thesis: verum