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 5;
Down V,B = V /\ ([#] (GX | B)) by PRE_TOPC:def 10;
then Down V,B in the topology of (GX | B) by A1, PRE_TOPC:def 9;
hence Down V,B is open by PRE_TOPC:def 5; :: thesis: verum