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