theorem Th25: :: SFMASTR3:27

for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st c <> aa holds
not FinSeqMin (f,aa,bb,c) destroys aa