let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location holds {aa,bb} c= UsedIntLoc (swap (f,aa,bb))
let f be FinSeq-Location ; :: thesis: {aa,bb} c= UsedIntLoc (swap (f,aa,bb))
set a = aa;
set b = bb;
set aux1 = 1 -stRWNotIn {aa,bb};
set aux2 = 2 -ndRWNotIn {aa,bb};
set i0 = (1 -stRWNotIn {aa,bb}) := (f,aa);
set i1 = (2 -ndRWNotIn {aa,bb}) := (f,bb);
set i2 = (f,aa) := (2 -ndRWNotIn {aa,bb});
set i3 = (f,bb) := (1 -stRWNotIn {aa,bb});
A1: UsedIntLoc (swap (f,aa,bb)) = (UsedIntLoc ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ';' ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:30
.= ((UsedIntLoc (((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ (UsedIntLoc ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:30
.= (((UsedIntLoc ((1 -stRWNotIn {aa,bb}) := (f,aa))) \/ (UsedIntLoc ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ (UsedIntLoc ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:31
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ (UsedIntLoc ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ (UsedIntLoc ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:17
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ (UsedIntLoc ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:17
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa}) \/ (UsedIntLoc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:17
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa}) \/ {(1 -stRWNotIn {aa,bb}),bb} by SF_MASTR:17 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb} or x in UsedIntLoc (swap (f,aa,bb)) )
assume A2: x in {aa,bb} ; :: thesis: x in UsedIntLoc (swap (f,aa,bb))

per cases ( x = aa or x = bb ) by A2, TARSKI:def 2;

suppose x = aa ; :: thesis: x in UsedIntLoc (swap (f,aa,bb))

then x in {(2 -ndRWNotIn {aa,bb}),aa} by TARSKI:def 2;
then x in ({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa} by XBOOLE_0:def 3;
hence x in UsedIntLoc (swap (f,aa,bb)) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = bb ; :: thesis: x in UsedIntLoc (swap (f,aa,bb))

then x in {(1 -stRWNotIn {aa,bb}),bb} by TARSKI:def 2;
hence x in UsedIntLoc (swap (f,aa,bb)) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;