let X, Y be non empty set ; 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:]; 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 ; ( ( not p in X implies X-section (E,p) = {} ) & ( not p in Y implies Y-section (E,p) = {} ) )
assume A7:
not p in Y
; Y-section (E,p) = {}
then
Y-section (E,p) is empty
;
hence
Y-section (E,p) = {}
; verum