theorem Th7: :: NDIFF10:7

for X, Y being RealNormSpace
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 )