theorem :: FINSEQ_3:151

for x, y being object
for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds
( f . 1 = y & f . 2 = x )