B = [#] (GX | B) by PRE_TOPC:def 10;
then reconsider q3 = p as Point of (GX | B) by A1;
let S, S' 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
S' = Component_of q ) implies S = S' )
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
S' = Component_of q2 ; :: thesis: S = S'
S = Component_of q3 by A3;
hence S = S' by A4; :: thesis: verum