let GX be TopSpace; :: thesis: ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds

A meets B )

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) implies not GX is connected ) by Th3;

hence ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds

A meets B ) by A1; :: thesis: verum

A meets B )

A1: now :: thesis: ( not GX is connected implies ex A, B being Subset of GX st

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) )

( ex A, B being Subset of GX st ( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) )

assume
not GX is connected
; :: thesis: ex A, B being Subset of GX st

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B )

then consider P, Q being Subset of GX such that

A2: [#] GX = P \/ Q and

A3: P,Q are_separated and

A4: P <> {} GX and

A5: Q <> {} GX ;

reconsider P = P, Q = Q as Subset of GX ;

A6: Q is open by A2, A3, Th4;

P is open by A2, A3, Th4;

hence ex A, B being Subset of GX st

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) by A2, A3, A4, A5, A6, Th1; :: thesis: verum

end;( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B )

then consider P, Q being Subset of GX such that

A2: [#] GX = P \/ Q and

A3: P,Q are_separated and

A4: P <> {} GX and

A5: Q <> {} GX ;

reconsider P = P, Q = Q as Subset of GX ;

A6: Q is open by A2, A3, Th4;

P is open by A2, A3, Th4;

hence ex A, B being Subset of GX st

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) by A2, A3, A4, A5, A6, Th1; :: thesis: verum

( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open & A misses B ) implies not GX is connected ) by Th3;

hence ( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds

A meets B ) by A1; :: thesis: verum