let I be set ; :: thesis: for A, X, B, Y being ManySortedSet of st A c= X & B c= Y holds
[|A,Y|] /\ [|X,B|] = [|A,B|]
let A, X, B, Y be ManySortedSet of ; :: thesis: ( A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|] )
assume A1: ( A c= X & 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 A2: i in I ; :: thesis: ([|A,Y|] /\ [|X,B|]) . i = [|A,B|] . i
then A3: ( A . i c= X . i & B . i c= Y . i ) by A1, PBOOLE:def 5;
thus ([|A,Y|] /\ [|X,B|]) . i = ([|A,Y|] . i) /\ ([|X,B|] . i) by A2, PBOOLE:def 8
.= [:(A . i),(Y . i):] /\ ([|X,B|] . i) by A2, PBOOLE:def 21
.= [:(A . i),(Y . i):] /\ [:(X . i),(B . i):] by A2, PBOOLE:def 21
.= [:(A . i),(B . i):] by A3, ZFMISC_1:124
.= [|A,B|] . i by A2, PBOOLE:def 21 ; :: thesis: verum

end;

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