let X, Y be 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 ) )
let E be Element of bool [:X,Y:]; for x, y being set st x in X & y in Y holds
( ( [x,y] in E implies x in Y-section (E,y) ) & ( x in Y-section (E,y) implies [x,y] in E ) & ( [x,y] in E implies y in X-section (E,x) ) & ( y in X-section (E,x) implies [x,y] in E ) )
let x, y be set ; ( x in X & y in Y implies ( ( [x,y] in E implies x in Y-section (E,y) ) & ( x in Y-section (E,y) implies [x,y] in E ) & ( [x,y] in E implies y in X-section (E,x) ) & ( y in X-section (E,x) implies [x,y] in E ) ) )
assume A1:
( x in X & y in Y )
; ( ( [x,y] in E implies x in Y-section (E,y) ) & ( x in Y-section (E,y) implies [x,y] in E ) & ( [x,y] in E implies y in X-section (E,x) ) & ( y in X-section (E,x) implies [x,y] in E ) )
hence
( ( [x,y] in E implies x in Y-section (E,y) ) & ( x in Y-section (E,y) implies [x,y] in E ) & ( [x,y] in E implies y in X-section (E,x) ) & ( y in X-section (E,x) implies [x,y] in E ) )
by A2, A3, A4; verum