let X, Y be non empty set ; :: thesis: for A being Subset of X
for B being Subset of Y
for p being set holds
( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )
let A be Subset of X; :: thesis: for B being Subset of Y
for p being set holds
( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )
let B be Subset of Y; :: thesis: for p being set holds
( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )
let p be set ; :: thesis: ( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )
set E = [:A,B:];
thus ( p in A implies X-section ([:A,B:],p) = B ) by RELAT_1:168; :: thesis: ( ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )

hereby :: thesis: ( ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )

assume A5: not p in A ; :: thesis: X-section ([:A,B:],p) = {}

now :: thesis: for y being set holds not y in X-section ([:A,B:],p)

let y be set ; :: thesis: not y in X-section ([:A,B:],p)
assume y in X-section ([:A,B:],p) ; :: thesis: contradiction
then ex y1 being Element of Y st
( y = y1 & [p,y1] in [:A,B:] ) ;
hence contradiction by A5, ZFMISC_1:87; :: thesis: verum

end;

then X-section ([:A,B:],p) is empty ;
hence X-section ([:A,B:],p) = {} ; :: thesis: verum

end;

hereby :: thesis: ( not p in B implies Y-section ([:A,B:],p) = {} )

assume A4: p in B ; :: thesis: Y-section ([:A,B:],p) = A

now :: thesis: for x being set st x in Y-section ([:A,B:],p) holds
x in A

let x be set ; :: thesis: ( x in Y-section ([:A,B:],p) implies x in A )
assume x in Y-section ([:A,B:],p) ; :: thesis: x in A
then ex x1 being Element of X st
( x = x1 & [x1,p] in [:A,B:] ) ;
hence x in A by ZFMISC_1:87; :: thesis: verum

end;

then A5: Y-section ([:A,B:],p) c= A ;

now :: thesis: for x being set st x in A holds
x in Y-section ([:A,B:],p)

let x be set ; :: thesis: ( x in A implies x in Y-section ([:A,B:],p) )
assume A6: x in A ; :: thesis: x in Y-section ([:A,B:],p)
then [x,p] in [:A,B:] by A4, ZFMISC_1:87;
hence x in Y-section ([:A,B:],p) by A6; :: thesis: verum

end;

then A c= Y-section ([:A,B:],p) ;
hence Y-section ([:A,B:],p) = A by A5; :: thesis: verum

end;

assume A7: not p in B ; :: thesis: Y-section ([:A,B:],p) = {}

now :: thesis: for x being set holds not x in Y-section ([:A,B:],p)

let x be set ; :: thesis: not x in Y-section ([:A,B:],p)
assume x in Y-section ([:A,B:],p) ; :: thesis: contradiction
then ex x1 being Element of X st
( x = x1 & [x1,p] in [:A,B:] ) ;
hence contradiction by A7, ZFMISC_1:87; :: thesis: verum

end;

then Y-section ([:A,B:],p) is empty ;
hence Y-section ([:A,B:],p) = {} ; :: thesis: verum