theorem Th5: :: FUNCTOR0:5

for A, B being set
for a being object holds ~ ([:A,B:] --> a) = [:B,A:] --> a