A2:
B = [#] (GX | B)
by PRE_TOPC:def 5;

then reconsider q3 = p as Point of (GX | B) by A1;

reconsider C = Component_of q3 as Subset of GX by A2, XBOOLE_1:1;

take C ; :: thesis: for q being Point of (GX | B) st q = p holds

C = Component_of q

thus for q being Point of (GX | B) st q = p holds

C = Component_of q ; :: thesis: verum

then reconsider q3 = p as Point of (GX | B) by A1;

reconsider C = Component_of q3 as Subset of GX by A2, XBOOLE_1:1;

take C ; :: thesis: for q being Point of (GX | B) st q = p holds

C = Component_of q

thus for q being Point of (GX | B) st q = p holds

C = Component_of q ; :: thesis: verum