let X, Y be RealNormSpace; :: thesis: for Z being Subset of [:X,Y:]
for x, y being object holds
( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )

let Z be Subset of [:X,Y:]; :: thesis: for x, y being object holds
( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )

let x, y be object ; :: thesis: ( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )
set I = Exch (Y,X);
hereby :: thesis: ( [y,x] in (Exch (Y,X)) " Z implies [x,y] in Z )
assume A1: [x,y] in Z ; :: thesis: [y,x] in (Exch (Y,X)) " Z
then consider x1 being Point of X, y1 being Point of Y such that
A2: [x,y] = [x1,y1] by PRVECT_3:18;
A3: ( x = x1 & y = y1 ) by ;
A4: [x,y] = (Exch (Y,X)) . (y1,x1) by
.= (Exch (Y,X)) . [y,x] by A3 ;
[y1,x1] in the carrier of [:Y,X:] ;
hence [y,x] in (Exch (Y,X)) " Z by ; :: thesis: verum
end;
assume A5: [y,x] in (Exch (Y,X)) " Z ; :: thesis: [x,y] in Z
then consider y1 being Point of Y, x1 being Point of X such that
A6: [y,x] = [y1,x1] by PRVECT_3:18;
A7: ( x = x1 & y = y1 ) by ;
(Exch (Y,X)) . [y,x] = (Exch (Y,X)) . (y1,x1) by A6
.= [x,y] by ;
hence [x,y] in Z by ; :: thesis: verum