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 A3: ( ( for q being Point of (GX | B) st q = p holds
S = Component_of q ) & ( for q2 being Point of (GX | B) st q2 = p holds
S' = Component_of q2 ) ) ; :: thesis: S = S'
B = the carrier of (GX | B)

proof

B = [#] (GX | B) by PRE_TOPC:def 10;
hence B = the carrier of (GX | B) ; :: thesis: verum

end;

then reconsider q3 = p as Point of (GX | B) by A1;
( S = Component_of q3 & S' = Component_of q3 ) by A3;
hence S = S' ; :: thesis: verum