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) = {} ;

then A10: (Cl P) /\ Q = {} ;

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

Cl P misses Q
by A5;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;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

then A10: (Cl P) /\ Q = {} ;

now :: thesis: not C c= P

hence
contradiction
by A1, A2, A4, A5, A9, Th16; :: thesis: verumassume
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;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