let X, Y be non empty set ; :: thesis: 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:]; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: ( ( [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 ) )
A2: now :: thesis: ( y in X-section (E,x) implies [x,y] in E )
assume y in X-section (E,x) ; :: thesis: [x,y] in E
then y in { y where y is Element of Y : [x,y] in E } by MEASUR11:def 4;
then ex y1 being Element of Y st
( y = y1 & [x,y1] in E ) ;
hence [x,y] in E ; :: thesis: verum
end;
A3: now :: thesis: ( [x,y] in E implies y in X-section (E,x) )
assume [x,y] in E ; :: thesis: y in X-section (E,x)
then y in { y where y is Element of Y : [x,y] in E } by A1;
hence y in X-section (E,x) by MEASUR11:def 4; :: thesis: verum
end;
A4: now :: thesis: ( x in Y-section (E,y) implies [x,y] in E )
assume x in Y-section (E,y) ; :: thesis: [x,y] in E
then x in { x where x is Element of X : [x,y] in E } by MEASUR11:def 5;
then ex x1 being Element of X st
( x = x1 & [x1,y] in E ) ;
hence [x,y] in E ; :: thesis: verum
end;
now :: thesis: ( [x,y] in E implies x in Y-section (E,y) )
assume [x,y] in E ; :: thesis: x in Y-section (E,y)
then x in { x where x is Element of X : [x,y] in E } by A1;
hence x in Y-section (E,y) by MEASUR11:def 5; :: thesis: verum
end;
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; :: thesis: verum