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))
A1: Down (B2,V) = B2 /\ V by CONNSP_3:def 5;
( Down ((B1 \/ B2),V) = (B1 \/ B2) /\ V & Down (B1,V) = B1 /\ V ) by CONNSP_3:def 5;
hence Down ((B1 \/ B2),V) = (Down (B1,V)) \/ (Down (B2,V)) by A1, XBOOLE_1:23; :: thesis: verum