let GX be TopSpace; :: thesis: for V, B being Subset of GX st V is open holds

Down (V,B) is open

let V, B be Subset of GX; :: thesis: ( V is open implies Down (V,B) is open )

assume V is open ; :: thesis: Down (V,B) is open

then A1: V in the topology of GX by PRE_TOPC:def 2;

Down (V,B) = V /\ ([#] (GX | B)) by PRE_TOPC:def 5;

then Down (V,B) in the topology of (GX | B) by A1, PRE_TOPC:def 4;

hence Down (V,B) is open by PRE_TOPC:def 2; :: thesis: verum

Down (V,B) is open

let V, B be Subset of GX; :: thesis: ( V is open implies Down (V,B) is open )

assume V is open ; :: thesis: Down (V,B) is open

then A1: V in the topology of GX by PRE_TOPC:def 2;

Down (V,B) = V /\ ([#] (GX | B)) by PRE_TOPC:def 5;

then Down (V,B) in the topology of (GX | B) by A1, PRE_TOPC:def 4;

hence Down (V,B) is open by PRE_TOPC:def 2; :: thesis: verum