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 )
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 ) )
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;
( ex A, B being Subset of GX st
( [#] 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