let X, Y be non empty set ; :: thesis: for E being Subset of [:X,Y:]
for p being set holds
( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )
let E be Subset of [:X,Y:]; :: thesis: for p being set holds
( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )
let p be set ; :: thesis: ( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )

hereby :: thesis: ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) )

assume A1: p in X ; :: thesis: X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p))

now :: thesis: for y being set st y in X-section (([:X,Y:] \ E),p) holds
y in Y \ (X-section (E,p))

let y be set ; :: thesis: ( y in X-section (([:X,Y:] \ E),p) implies y in Y \ (X-section (E,p)) )
assume A2: y in X-section (([:X,Y:] \ E),p) ; :: thesis: y in Y \ (X-section (E,p))
then A3: ex y1 being Element of Y st
( y = y1 & [p,y1] in [:X,Y:] \ E ) ;

now :: thesis: not y in X-section (E,p)

assume y in X-section (E,p) ; :: thesis: contradiction
then ex y2 being Element of Y st
( y = y2 & [p,y2] in E ) ;
hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

end;

hence y in Y \ (X-section (E,p)) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

then A4: X-section (([:X,Y:] \ E),p) c= Y \ (X-section (E,p)) ;

now :: thesis: for y being set st y in Y \ (X-section (E,p)) holds
y in X-section (([:X,Y:] \ E),p)

let y be set ; :: thesis: ( y in Y \ (X-section (E,p)) implies y in X-section (([:X,Y:] \ E),p) )
assume A5: y in Y \ (X-section (E,p)) ; :: thesis: y in X-section (([:X,Y:] \ E),p)
then ( y in Y & not y in X-section (E,p) ) by XBOOLE_0:def 5;
then A6: not [p,y] in E ;
[p,y] in [:X,Y:] by A1, A5, ZFMISC_1:def 2;
then [p,y] in [:X,Y:] \ E by A6, XBOOLE_0:def 5;
hence y in X-section (([:X,Y:] \ E),p) by A5; :: thesis: verum

end;

then Y \ (X-section (E,p)) c= X-section (([:X,Y:] \ E),p) ;
hence X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) by A4; :: thesis: verum

end;

assume A7: p in Y ; :: thesis: Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p))

now :: thesis: for y being set st y in Y-section (([:X,Y:] \ E),p) holds
y in X \ (Y-section (E,p))

let y be set ; :: thesis: ( y in Y-section (([:X,Y:] \ E),p) implies y in X \ (Y-section (E,p)) )
assume A8: y in Y-section (([:X,Y:] \ E),p) ; :: thesis: y in X \ (Y-section (E,p))
then A9: ex y1 being Element of X st
( y = y1 & [y1,p] in [:X,Y:] \ E ) ;

now :: thesis: not y in Y-section (E,p)

assume y in Y-section (E,p) ; :: thesis: contradiction
then ex y2 being Element of X st
( y = y2 & [y2,p] in E ) ;
hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum

end;

hence y in X \ (Y-section (E,p)) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then A10: Y-section (([:X,Y:] \ E),p) c= X \ (Y-section (E,p)) ;

now :: thesis: for y being set st y in X \ (Y-section (E,p)) holds
y in Y-section (([:X,Y:] \ E),p)

let y be set ; :: thesis: ( y in X \ (Y-section (E,p)) implies y in Y-section (([:X,Y:] \ E),p) )
assume A11: y in X \ (Y-section (E,p)) ; :: thesis: y in Y-section (([:X,Y:] \ E),p)
then ( y in X & not y in Y-section (E,p) ) by XBOOLE_0:def 5;
then A12: not [y,p] in E ;
[y,p] in [:X,Y:] by A7, A11, ZFMISC_1:def 2;
then [y,p] in [:X,Y:] \ E by A12, XBOOLE_0:def 5;
hence y in Y-section (([:X,Y:] \ E),p) by A11; :: thesis: verum

end;

then X \ (Y-section (E,p)) c= Y-section (([:X,Y:] \ E),p) ;
hence Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) by A10; :: thesis: verum