let I be set ; :: thesis: for A, x, y, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds
A in [|(x /\ X),(y /\ Y)|]
let A, x, y, 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 set ; :: 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, PBOOLE:def 1;
A5: A . i in [|X,Y|] . i by A2, A3, PBOOLE:def 1;
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