let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of st ( x1 /\ x2 = [0] I or A /\ B = [0] I ) holds
[|x1,A|] /\ [|x2,B|] = [0] I
let x1, x2, A, B be ManySortedSet of ; :: thesis: ( ( x1 /\ x2 = [0] I or A /\ B = [0] I ) implies [|x1,A|] /\ [|x2,B|] = [0] I )
assume A1: ( x1 /\ x2 = [0] I or A /\ B = [0] I ) ; :: thesis: [|x1,A|] /\ [|x2,B|] = [0] I

per cases ( x1 /\ x2 = [0] I or A /\ B = [0] I ) by A1;

suppose A2: x1 /\ x2 = [0] I ; :: thesis: [|x1,A|] /\ [|x2,B|] = [0] I

now

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

end;

hence [|x1,A|] /\ [|x2,B|] = [0] I by PBOOLE:3; :: thesis: verum

end;

suppose A5: A /\ B = [0] I ; :: thesis: [|x1,A|] /\ [|x2,B|] = [0] I

now

let i be set ; :: thesis: ( i in I implies ([|x1,A|] /\ [|x2,B|]) . i = ([0] I) . i )
assume A6: i in I ; :: thesis: ([|x1,A|] /\ [|x2,B|]) . i = ([0] I) . i
then (A . i) /\ (B . i) = (A /\ B) . i by PBOOLE:def 8
.= {} by A5, PBOOLE:5 ;
then A . i misses B . i by XBOOLE_0:def 7;
then A7: [:(x1 . i),(A . i):] misses [:(x2 . i),(B . i):] by ZFMISC_1:127;
thus ([|x1,A|] /\ [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A6, PBOOLE:def 8
.= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A6, PBOOLE:def 21
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A6, PBOOLE:def 21
.= {} by A7, XBOOLE_0:def 7
.= ([0] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|x1,A|] /\ [|x2,B|] = [0] I by PBOOLE:3; :: thesis: verum

end;

end;