let GX be TopSpace; :: thesis: ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined )

A1: now :: thesis: ( ex a being Point of GX st
for x being Point of GX holds a,x are_joined implies for x, y being Point of GX holds x,y are_joined )

given a being Point of GX such that A2: for x being Point of GX holds a,x are_joined ; :: thesis: for x, y being Point of GX holds x,y are_joined
let x, y be Point of GX; :: thesis: x,y are_joined
a,x are_joined by A2;
then consider C1 being Subset of GX such that
A3: C1 is connected and
A4: a in C1 and
A5: x in C1 ;
a,y are_joined by A2;
then consider C2 being Subset of GX such that
A6: C2 is connected and
A7: a in C2 and
A8: y in C2 ;
C1 /\ C2 <> {} GX by A4, A7, XBOOLE_0:def 4;
then C1 meets C2 ;
then A9: C1 \/ C2 is connected by A3, A6, Th1, Th17;
A10: y in C1 \/ C2 by A8, XBOOLE_0:def 3;
x in C1 \/ C2 by A5, XBOOLE_0:def 3;
hence x,y are_joined by A9, A10; :: thesis: verum

end;

now :: thesis: ( ( for x, y being Point of GX holds x,y are_joined ) implies ex x being Point of GX st
for y being Point of GX holds x,y are_joined )

set a = the Point of GX;
assume for x, y being Point of GX holds x,y are_joined ; :: thesis: ex x being Point of GX st
for y being Point of GX holds x,y are_joined
then for y being Point of GX holds the Point of GX,y are_joined ;
hence ex x being Point of GX st
for y being Point of GX holds x,y are_joined ; :: thesis: verum

end;

hence ( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined ) by A1; :: thesis: verum