theorem Th14: :: SETLIM_2:14
for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (\) A2) c= (Intersection A1) \ (Intersection A2)