theorem Th53: :: FUNCT_3:53

for X, Y being set holds <:(pr1 (X,Y)),(pr2 (X,Y)):> = id [:X,Y:]