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