theorem Th5: :: YELLOW12:5

for A, B, X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:]