let I be set ; :: thesis: for x, y, A, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds
A in [|(x (/\) X),(y (/\) Y)|]
let x, y, A, X, Y be ManySortedSet of I; :: thesis: ( A in [|x,y|] & A in [|X,Y|] implies A in [|(x (/\) X),(y (/\) Y)|] )
assume that
A1: A in [|x,y|] and
A2: A in [|X,Y|] ; :: thesis: A in [|(x (/\) X),(y (/\) Y)|]
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in [|(x (/\) X),(y (/\) Y)|] . i )
assume A3: i in I ; :: thesis: A . i in [|(x (/\) X),(y (/\) Y)|] . i
then A4: A . i in [|x,y|] . i by A1;
A5: A . i in [|X,Y|] . i by A2, A3;
A6: A . i in [:(x . i),(y . i):] by A3, A4, PBOOLE:def 16;
A . i in [:(X . i),(Y . i):] by A3, A5, PBOOLE:def 16;
then A . i in [:((x . i) /\ (X . i)),((y . i) /\ (Y . i)):] by A6, ZFMISC_1:113;
then A . i in [:((x (/\) X) . i),((y . i) /\ (Y . i)):] by A3, PBOOLE:def 5;
then A . i in [:((x (/\) X) . i),((y (/\) Y) . i):] by A3, PBOOLE:def 5;
hence A . i in [|(x (/\) X),(y (/\) Y)|] . i by A3, PBOOLE:def 16; :: thesis: verum