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
B: for n being Nat holds B . n = A by VALUED_0:def 18;
for n being Element of NAT holds B . n = A by B;
then ( Union B = A & Intersection B = A ) by Th185, Th186;
hence Union B = Intersection B ; :: thesis: verum