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 ) )
thus 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 ) )
thus 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 )
thus ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) by A3, A4, Th16; :: thesis: verum