B = the carrier of (GX | B)

proof

B = [#] (GX | B) by PRE_TOPC:def 10;
hence B = the carrier of (GX | B) ; :: thesis: verum

end;

hence p is Point of (GX | B) by A1; :: thesis: verum