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