B = [#] (GX | B) by PRE_TOPC:def 5;
then reconsider q3 = p as Point of (GX | B) by A1;
let S, S9 be Subset of GX; :: thesis: ( ( for q being Point of (GX | B) st q = p holds
S = Component_of q ) & ( for q being Point of (GX | B) st q = p holds
S9 = Component_of q ) implies S = S9 )
assume that
A3: for q being Point of (GX | B) st q = p holds
S = Component_of q and
A4: for q2 being Point of (GX | B) st q2 = p holds
S9 = Component_of q2 ; :: thesis: S = S9
S = Component_of q3 by A3;
hence S = S9 by A4; :: thesis: verum