let x, y, X, Y be set ; :: thesis: ( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] )
( ( [x,y] in [:X,Y:] implies ( x in X & y in Y ) ) & ( y in Y & x in X implies [y,x] in [:Y,X:] ) ) by Lm17;
hence ( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] ) ; :: thesis: verum