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