let X be set ; :: thesis: for B being SetSequence of X holds Intersection B c= Union B
let B be SetSequence of X; :: thesis: Intersection B c= Union B
meet (rng B) c= union (rng B) by SETFAM_1:2;
then Intersection B c= union (rng B) by Th8;
hence Intersection B c= Union B by CARD_3:def 4; :: thesis: verum