let I be set ; :: thesis: for A, B being ManySortedSet of holds Intersect A,B = A /\ B
let A, B be ManySortedSet of ; :: thesis: Intersect A,B = A /\ B
A1: ( dom A = I & dom B = I ) by PARTFUN1:def 4;
then dom (Intersect A,B) = I /\ I by Def2;
then reconsider AB = Intersect A,B as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
I /\ I = I ;
then for i being set st i in I holds
AB . i = (A . i) /\ (B . i) by A1, Def2;
hence Intersect A,B = A /\ B by PBOOLE:def 8; :: thesis: verum