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

A5: now

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