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