let I be set ; :: thesis: for A, X, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X (/\) Y c= A
let A, X, Y be ManySortedSet of I; :: thesis: ( ( X c= A or Y c= A ) implies X (/\) Y c= A )
assume A1: ( X c= A or Y c= A ) ; :: thesis: X (/\) Y c= A

per cases ( X c= A or Y c= A ) by A1;

suppose A2: X c= A ; :: thesis: X (/\) Y c= A

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (X (/\) Y) . i c= A . i )
assume A3: i in I ; :: thesis: (X (/\) Y) . i c= A . i
then X . i c= A . i by A2;
then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence (X (/\) Y) . i c= A . i by A3, PBOOLE:def 5; :: thesis: verum

end;

suppose A4: Y c= A ; :: thesis: X (/\) Y c= A

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (X (/\) Y) . i c= A . i )
assume A5: i in I ; :: thesis: (X (/\) Y) . i c= A . i
then Y . i c= A . i by A4;
then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence (X (/\) Y) . i c= A . i by A5, PBOOLE:def 5; :: thesis: verum

end;

end;