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 )

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

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 )

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;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

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 )

hence
( 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;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

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