theorem Th13: :: SETLIM_2:13

for X being set
for A1, A2 being SetSequence of X holds (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)