let I be set ; :: thesis: for X, Y being ManySortedSet of st X /\ Y = [0] I holds
[|X,Y|] /\ [|Y,X|] = [0] I
let X, Y be ManySortedSet of ; :: thesis: ( X /\ Y = [0] I implies [|X,Y|] /\ [|Y,X|] = [0] I )
assume A1: X /\ Y = [0] I ; :: thesis: [|X,Y|] /\ [|Y,X|] = [0] I

now

let i be set ; :: thesis: ( i in I implies ([|X,Y|] /\ [|Y,X|]) . i = ([0] I) . i )
assume A2: i in I ; :: thesis: ([|X,Y|] /\ [|Y,X|]) . i = ([0] I) . i
then (X . i) /\ (Y . i) = (X /\ Y) . i by PBOOLE:def 8
.= {} by A1, PBOOLE:5 ;
then X . i misses Y . i by XBOOLE_0:def 7;
then A3: [:(X . i),(Y . i):] misses [:(Y . i),(X . i):] by ZFMISC_1:127;
thus ([|X,Y|] /\ [|Y,X|]) . i = ([|X,Y|] . i) /\ ([|Y,X|] . i) by A2, PBOOLE:def 8
.= [:(X . i),(Y . i):] /\ ([|Y,X|] . i) by A2, PBOOLE:def 21
.= [:(X . i),(Y . i):] /\ [:(Y . i),(X . i):] by A2, PBOOLE:def 21
.= {} by A3, XBOOLE_0:def 7
.= ([0] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|X,Y|] /\ [|Y,X|] = [0] I by PBOOLE:3; :: thesis: verum