theorem Th8: :: YELLOW12:8

for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):>