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

now :: thesis: for q being set holds not q in X-section (({} [:X,Y:]),p)

let q be set ; :: thesis: not q in X-section (({} [:X,Y:]),p)
assume q in X-section (({} [:X,Y:]),p) ; :: thesis: contradiction
then ex y1 being Element of Y st
( q = y1 & [p,y1] in {} [:X,Y:] ) ;
hence contradiction ; :: thesis: verum

end;

then X-section (({} [:X,Y:]),p) is empty ;
hence X-section (({} [:X,Y:]),p) = {} ; :: thesis: ( Y-section (({} [:X,Y:]),p) = {} & ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) & ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) )

now :: thesis: for q being set holds not q in Y-section (({} [:X,Y:]),p)

let q be set ; :: thesis: not q in Y-section (({} [:X,Y:]),p)
assume q in Y-section (({} [:X,Y:]),p) ; :: thesis: contradiction
then ex x1 being Element of X st
( q = x1 & [x1,p] in {} [:X,Y:] ) ;
hence contradiction ; :: thesis: verum

end;

then Y-section (({} [:X,Y:]),p) is empty ;
hence Y-section (({} [:X,Y:]),p) = {} ; :: thesis: ( ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) & ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) )
A3: ( [#] X = X & [#] Y = Y ) by SUBSET_1:def 3;
then A4: [#] [:X,Y:] = [:([#] X),([#] Y):] by SUBSET_1:def 3;
hence ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) by A3, Th16; :: thesis: ( p in Y implies Y-section (([#] [:X,Y:]),p) = X )
assume p in Y ; :: thesis: Y-section (([#] [:X,Y:]),p) = X
hence Y-section (([#] [:X,Y:]),p) = X by A3, A4, Th16; :: thesis: verum