let X be set ; :: thesis: for B being SetSequence of X st B is constant holds

Union B = Intersection B

let B be SetSequence of X; :: thesis: ( B is constant implies Union B = Intersection B )

assume B is constant ; :: thesis: Union B = Intersection B

then consider A being Subset of X such that

A1: for n being Nat holds B . n = A by VALUED_0:def 18;

Union B = A by Th10, A1;

hence Union B = Intersection B by Th11, A1; :: thesis: verum

Union B = Intersection B

let B be SetSequence of X; :: thesis: ( B is constant implies Union B = Intersection B )

assume B is constant ; :: thesis: Union B = Intersection B

then consider A being Subset of X such that

A1: for n being Nat holds B . n = A by VALUED_0:def 18;

Union B = A by Th10, A1;

hence Union B = Intersection B by Th11, A1; :: thesis: verum