theorem Th4: :: YELLOW12:4

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