theorem :: YELLOW_7:46

for L being non empty RelStr
for J being set
for K being ManySortedSet of J
for x being set holds
( x is DoubleIndexedSet of K,L iff x is DoubleIndexedSet of K,(L opp) ) ;