theorem :: GOBRD11:4
for GX being non empty TopSpace
for B1, B2, V being Subset of GX holds Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V))