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;
A2: for n being Element of NAT holds B . n = A by A1;
then Union B = A by Th10;
hence Union B = Intersection B by A2, Th11; :: thesis: verum