let GX be non empty TopSpace; :: thesis: for B1, B2, V being Subset of GX holds Down (B1 \/ B2),V = (Down B1,V) \/ (Down B2,V)
let B1, B2, V be Subset of GX; :: thesis: Down (B1 \/ B2),V = (Down B1,V) \/ (Down B2,V)
( Down (B1 \/ B2),V = (B1 \/ B2) /\ V & Down B1,V = B1 /\ V & Down B2,V = B2 /\ V ) by CONNSP_3:def 5;
hence Down (B1 \/ B2),V = (Down B1,V) \/ (Down B2,V) by XBOOLE_1:23; :: thesis: verum