let GX be TopSpace; :: thesis: for A, C being Subset of GX st C is connected & C c= A & A c= Cl C holds
A is connected
let A, C be Subset of GX; :: thesis: ( C is connected & C c= A & A c= Cl C implies A is connected )
assume that
A1: C is connected and
A2: C c= A and
A3: A c= Cl C ; :: thesis: A is connected
assume not A is connected ; :: thesis: contradiction
then consider P, Q being Subset of GX such that
A4: A = P \/ Q and
A5: P,Q are_separated and
A6: P <> {} GX and
A7: Q <> {} GX by Th15;
P misses Cl Q by A5;
then A8: P /\ (Cl Q) = {} ;
A9: now :: thesis: not C c= Q
assume C c= Q ; :: thesis: contradiction
then Cl C c= Cl Q by PRE_TOPC:19;
then P /\ (Cl C) = {} by A8, XBOOLE_1:3, XBOOLE_1:27;
then P /\ A = {} by A3, XBOOLE_1:3, XBOOLE_1:27;
hence contradiction by A4, A6, XBOOLE_1:21; :: thesis: verum
end;
Cl P misses Q by A5;
then A10: (Cl P) /\ Q = {} ;
now :: thesis: not C c= P
assume C c= P ; :: thesis: contradiction
then Cl C c= Cl P by PRE_TOPC:19;
then (Cl C) /\ Q = {} by A10, XBOOLE_1:3, XBOOLE_1:27;
then A /\ Q = {} by A3, XBOOLE_1:3, XBOOLE_1:27;
hence contradiction by A4, A7, XBOOLE_1:21; :: thesis: verum
end;
hence contradiction by A1, A2, A4, A5, A9, Th16; :: thesis: verum