let I be set ; :: thesis: for A, X, B, Y being ManySortedSet of I st A c= X & B c= Y holds
[|A,Y|] /\ [|X,B|] = [|A,B|]
let A, X, B, Y be ManySortedSet of I; :: thesis: ( A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|] )
assume that
A1: A c= X and
A2: B c= Y ; :: thesis: [|A,Y|] /\ [|X,B|] = [|A,B|]

now

let i be set ; :: thesis: ( i in I implies ([|A,Y|] /\ [|X,B|]) . i = [|A,B|] . i )
assume A3: i in I ; :: thesis: ([|A,Y|] /\ [|X,B|]) . i = [|A,B|] . i
then A4: A . i c= X . i by A1, PBOOLE:def 2;
A5: B . i c= Y . i by A2, A3, PBOOLE:def 2;
thus ([|A,Y|] /\ [|X,B|]) . i = ([|A,Y|] . i) /\ ([|X,B|] . i) by A3, PBOOLE:def 5
.= [:(A . i),(Y . i):] /\ ([|X,B|] . i) by A3, PBOOLE:def 16
.= [:(A . i),(Y . i):] /\ [:(X . i),(B . i):] by A3, PBOOLE:def 16
.= [:(A . i),(B . i):] by A4, A5, ZFMISC_1:101
.= [|A,B|] . i by A3, PBOOLE:def 16 ; :: thesis: verum

end;

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