A2: B = [#] (GX | B) by PRE_TOPC:def 10;
then reconsider q3 = p as Point of by A1;
reconsider C = Component_of q3 as Subset of by A2, XBOOLE_1:1;
take C ; :: thesis: for q being Point of st q = p holds
C = Component_of q
thus for q being Point of st q = p holds
C = Component_of q ; :: thesis: verum