theorem Th25: :: MESFUN12:25

for X, Y being non empty set
for A being Element of bool [:X,Y:]
for x, y being set st x in X & y in Y holds
( ( [x,y] in A implies x in Y-section (A,y) ) & ( x in Y-section (A,y) implies [x,y] in A ) & ( [x,y] in A implies y in X-section (A,x) ) & ( y in X-section (A,x) implies [x,y] in A ) )