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