B = the carrier of (GX | B) by PRE_TOPC:8;
then p in B by A1;
hence p is Point of GX ; :: thesis: verum