theorem Th18: :: YELLOW20:18

for I, J being set
for F1, F2 being ManySortedSet of [:I,I:]
for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )