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

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