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

hereby :: thesis: ( not p in Y implies Y-section (E,p) = {} )

assume A1: not p in X ; :: thesis: X-section (E,p) = {}

now :: thesis: for y being set holds not y in X-section (E,p)

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

end;

then X-section (E,p) is empty ;
hence X-section (E,p) = {} ; :: thesis: verum

end;

assume A7: not p in Y ; :: thesis: Y-section (E,p) = {}

now :: thesis: for y being set holds not y in Y-section (E,p)

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

end;

then Y-section (E,p) is empty ;
hence Y-section (E,p) = {} ; :: thesis: verum