B = [#] (GX | B) by PRE_TOPC:def 5;
hence p is Point of (GX | B) by A1; :: thesis: verum