let I, J be set ; :: thesis: for A being ManySortedSet of I
for B being ManySortedSet of J holds Intersect A,B is ManySortedSet of I /\ J
let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J holds Intersect A,B is ManySortedSet of I /\ J
let B be ManySortedSet of J; :: thesis: Intersect A,B is ManySortedSet of I /\ J
( dom A = I & dom B = J ) by PBOOLE:def 3;
hence dom (Intersect A,B) = I /\ J by Def2; :: according to PBOOLE:def 3 :: thesis: verum