theorem Th30: :: SFMASTR3:32

for aa, bb, cc being Int-Location
for f being FinSeq-Location st cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} holds
not swap (f,aa,bb) destroys cc