let x, y be object ; for X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]
let X, Y be set ; ( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] )
( [x,y] in [:X,Y:] implies ( x in X & y in Y ) )
by Lm16;
hence
( [x,y] in [:X,Y:] implies [y,x] in [:Y,X:] )
by Lm16; verum