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