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

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