theorem :: FINSEQ_5:61

for x1, x2 being object holds Rev <*x1,x2*> = <*x2,x1*>