let GX be TopSpace; :: thesis: for X' being SubSpace of GX
for A being Subset of
for B being Subset of st A = B holds
( A is connected iff B is connected )
let X' be SubSpace of GX; :: thesis: for A being Subset of
for B being Subset of st A = B holds
( A is connected iff B is connected )
let A be Subset of ; :: thesis: for B being Subset of st A = B holds
( A is connected iff B is connected )
let B be Subset of ; :: thesis: ( A = B implies ( A is connected iff B is connected ) )
assume A1: A = B ; :: thesis: ( A is connected iff B is connected )
reconsider GX' = GX, X = X' as TopSpace ;
A2: [#] (GX | A) = A by PRE_TOPC:def 10;
reconsider B' = B as Subset of ;
reconsider A' = A as Subset of ;
A3: [#] (X' | B) = B by PRE_TOPC:def 10;
A4: {} (GX | A) = {} (X' | B) ;

A5: now

assume not A is connected ; :: thesis: not B is connected
then not GX' | A' is connected by Def3;
then consider P, Q being Subset of such that
A6: [#] (GX | A) = P \/ Q and
A7: P <> {} (GX | A) and
A8: Q <> {} (GX | A) and
A9: P is closed and
A10: Q is closed and
A11: P misses Q by Th11;
consider P1 being Subset of such that
A12: P1 is closed and
A13: P1 /\ ([#] (GX | A)) = P by A9, PRE_TOPC:43;
reconsider P11 = P1 /\ ([#] X') as Subset of ;
A14: P11 is closed by A12, PRE_TOPC:43;
reconsider PP = P, QQ = Q as Subset of by A1, A2, A3;
A15: P c= [#] X' by A1, A2, XBOOLE_1:1;
P1 /\ A c= P1 by XBOOLE_1:17;
then P c= P1 /\ ([#] X') by A2, A13, A15, XBOOLE_1:19;
then A16: P c= (P1 /\ ([#] X')) /\ A by A2, XBOOLE_1:19;
P1 /\ ([#] X') c= P1 by XBOOLE_1:17;
then (P1 /\ ([#] X')) /\ A c= P by A2, A13, XBOOLE_1:27;
then P11 /\ ([#] (X' | B)) = PP by A1, A3, A16, XBOOLE_0:def 10;
then A17: PP is closed by A14, PRE_TOPC:43;
consider Q1 being Subset of such that
A18: Q1 is closed and
A19: Q1 /\ ([#] (GX | A)) = Q by A10, PRE_TOPC:43;
reconsider Q11 = Q1 /\ ([#] X') as Subset of ;
A20: Q c= [#] X' by A1, A2, XBOOLE_1:1;
Q1 /\ A c= Q1 by XBOOLE_1:17;
then Q c= Q1 /\ ([#] X') by A2, A19, A20, XBOOLE_1:19;
then A21: Q c= (Q1 /\ ([#] X')) /\ A by A2, XBOOLE_1:19;
Q1 /\ ([#] X') c= Q1 by XBOOLE_1:17;
then (Q1 /\ ([#] X')) /\ A c= Q by A2, A19, XBOOLE_1:27;
then A22: (Q1 /\ ([#] X')) /\ A = Q by A21, XBOOLE_0:def 10;
Q11 is closed by A18, PRE_TOPC:43;
then QQ is closed by A1, A3, A22, PRE_TOPC:43;
then not X | B' is connected by A1, A2, A3, A4, A6, A7, A8, A11, A17, Th11;
hence not B is connected by Def3; :: thesis: verum

end;

now

assume not B is connected ; :: thesis: not A is connected
then not X' | B is connected by Def3;
then consider P, Q being Subset of such that
A23: [#] (X' | B) = P \/ Q and
A24: P <> {} (X' | B) and
A25: Q <> {} (X' | B) and
A26: P is closed and
A27: Q is closed and
A28: P misses Q by Th11;
reconsider QQ = Q as Subset of by A1, A2, A3;
reconsider PP = P as Subset of by A1, A2, A3;
consider P1 being Subset of such that
A29: P1 is closed and
A30: P1 /\ ([#] (X' | B)) = P by A26, PRE_TOPC:43;
consider Q1 being Subset of such that
A31: Q1 is closed and
A32: Q1 /\ ([#] (X' | B)) = Q by A27, PRE_TOPC:43;
consider Q2 being Subset of such that
A33: Q2 is closed and
A34: Q2 /\ ([#] X') = Q1 by A31, PRE_TOPC:43;
Q2 /\ ([#] (GX | A)) = Q2 /\ (([#] X') /\ B) by A1, A2, XBOOLE_1:28
.= QQ by A3, A32, A34, XBOOLE_1:16 ;
then A35: QQ is closed by A33, PRE_TOPC:43;
consider P2 being Subset of such that
A36: P2 is closed and
A37: P2 /\ ([#] X') = P1 by A29, PRE_TOPC:43;
P2 /\ ([#] (GX | A)) = P2 /\ (([#] X') /\ B) by A1, A2, XBOOLE_1:28
.= PP by A3, A30, A37, XBOOLE_1:16 ;
then PP is closed by A36, PRE_TOPC:43;
then not GX' | A' is connected by A1, A2, A3, A4, A23, A24, A25, A28, A35, Th11;
hence not A is connected by Def3; :: thesis: verum

end;

hence ( A is connected iff B is connected ) by A5; :: thesis: verum