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 by CONNSP_3:def 5;

then A1: Down ((B1 /\ B2),V) = B1 /\ (B2 /\ (V /\ V)) by XBOOLE_1:16

.= B1 /\ ((B2 /\ V) /\ V) by XBOOLE_1:16

.= (B1 /\ V) /\ (B2 /\ V) by XBOOLE_1:16 ;

Down (B1,V) = B1 /\ V by CONNSP_3:def 5;

hence Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) by A1, CONNSP_3:def 5; :: thesis: verum

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 by CONNSP_3:def 5;

then A1: Down ((B1 /\ B2),V) = B1 /\ (B2 /\ (V /\ V)) by XBOOLE_1:16

.= B1 /\ ((B2 /\ V) /\ V) by XBOOLE_1:16

.= (B1 /\ V) /\ (B2 /\ V) by XBOOLE_1:16 ;

Down (B1,V) = B1 /\ V by CONNSP_3:def 5;

hence Down ((B1 /\ B2),V) = (Down (B1,V)) /\ (Down (B2,V)) by A1, CONNSP_3:def 5; :: thesis: verum