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

A4: 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 (GX | A) such that
A5: [#] (GX | A) = P \/ Q and
A6: P <> {} (GX | A) and
A7: Q <> {} (GX | A) and
A8: P is closed and
A9: Q is closed and
A10: P misses Q by Th11;
consider P1 being Subset of GX such that
A11: P1 is closed and
A12: P1 /\ ([#] (GX | A)) = P by A8, PRE_TOPC:43;
consider Q1 being Subset of GX such that
A13: Q1 is closed and
A14: Q1 /\ ([#] (GX | A)) = Q by A9, PRE_TOPC:43;
reconsider PP = P, QQ = Q as Subset of (X' | B) by A1, A2;
reconsider P11 = P1 /\ ([#] X') as Subset of X' ;
A15: P11 is closed by A11, PRE_TOPC:43;
( P1 /\ ([#] X') c= P1 & A c= A ) by XBOOLE_1:17;
then A16: (P1 /\ ([#] X')) /\ A c= P by A2, A12, XBOOLE_1:27;
A17: P1 /\ A c= P1 by XBOOLE_1:17;
P c= [#] X' by A1, A2, XBOOLE_1:1;
then P c= P1 /\ ([#] X') by A2, A12, A17, XBOOLE_1:19;
then P c= (P1 /\ ([#] X')) /\ A by A2, XBOOLE_1:19;
then P11 /\ ([#] (X' | B)) = PP by A1, A2, A16, XBOOLE_0:def 10;
then A18: PP is closed by A15, PRE_TOPC:43;
reconsider Q11 = Q1 /\ ([#] X') as Subset of X' ;
A19: Q11 is closed by A13, PRE_TOPC:43;
( Q1 /\ ([#] X') c= Q1 & A c= A ) by XBOOLE_1:17;
then A20: (Q1 /\ ([#] X')) /\ A c= Q by A2, A14, XBOOLE_1:27;
A21: Q1 /\ A c= Q1 by XBOOLE_1:17;
Q c= [#] X' by A1, A2, XBOOLE_1:1;
then Q c= Q1 /\ ([#] X') by A2, A14, A21, XBOOLE_1:19;
then Q c= (Q1 /\ ([#] X')) /\ A by A2, XBOOLE_1:19;
then (Q1 /\ ([#] X')) /\ A = Q by A20, XBOOLE_0:def 10;
then QQ is closed by A1, A2, A19, PRE_TOPC:43;
then not X | B' is connected by A1, A2, A3, A5, A6, A7, A10, A18, 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 (X' | B) such that
A22: [#] (X' | B) = P \/ Q and
A23: P <> {} (X' | B) and
A24: Q <> {} (X' | B) and
A25: P is closed and
A26: Q is closed and
A27: P misses Q by Th11;
consider P1 being Subset of X' such that
A28: P1 is closed and
A29: P1 /\ ([#] (X' | B)) = P by A25, PRE_TOPC:43;
consider Q1 being Subset of X' such that
A30: Q1 is closed and
A31: Q1 /\ ([#] (X' | B)) = Q by A26, PRE_TOPC:43;
consider P2 being Subset of GX such that
A32: P2 is closed and
A33: P2 /\ ([#] X') = P1 by A28, PRE_TOPC:43;
consider Q2 being Subset of GX such that
A34: Q2 is closed and
A35: Q2 /\ ([#] X') = Q1 by A30, PRE_TOPC:43;
reconsider PP = P as Subset of (GX | A) by A1, A2;
reconsider QQ = Q as Subset of (GX | A) by A1, A2;
P2 /\ ([#] (GX | A)) = P2 /\ (([#] X') /\ B) by A1, A2, XBOOLE_1:28
.= PP by A2, A29, A33, XBOOLE_1:16 ;
then A36: PP is closed by A32, PRE_TOPC:43;
Q2 /\ ([#] (GX | A)) = Q2 /\ (([#] X') /\ B) by A1, A2, XBOOLE_1:28
.= QQ by A2, A31, A35, XBOOLE_1:16 ;
then QQ is closed by A34, PRE_TOPC:43;
then not GX' | A' is connected by A1, A2, A3, A22, A23, A24, A27, A36, Th11;
hence not A is connected by Def3; :: thesis: verum

end;

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