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

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

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

now :: thesis: for i being object st i in I holds
([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies ([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i )
assume A3: i in I ; :: thesis: ([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i
then (x1 . i) /\ (x2 . i) = (x1 (/\) x2) . i by PBOOLE:def 5
.= {} 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:104;
thus ([|x1,A|] (/\) [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A3, PBOOLE:def 5
.= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A3, PBOOLE:def 16
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A3, PBOOLE:def 16
.= {} by A4, XBOOLE_0:def 7
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|x1,A|] (/\) [|x2,B|] = EmptyMS I ; :: thesis: verum

end;

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

now :: thesis: for i being object st i in I holds
([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies ([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i )
assume A6: i in I ; :: thesis: ([|x1,A|] (/\) [|x2,B|]) . i = (EmptyMS I) . i
then (A . i) /\ (B . i) = (A (/\) B) . i by PBOOLE:def 5
.= {} 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:104;
thus ([|x1,A|] (/\) [|x2,B|]) . i = ([|x1,A|] . i) /\ ([|x2,B|] . i) by A6, PBOOLE:def 5
.= [:(x1 . i),(A . i):] /\ ([|x2,B|] . i) by A6, PBOOLE:def 16
.= [:(x1 . i),(A . i):] /\ [:(x2 . i),(B . i):] by A6, PBOOLE:def 16
.= {} by A7, XBOOLE_0:def 7
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence [|x1,A|] (/\) [|x2,B|] = EmptyMS I ; :: thesis: verum

end;

end;