let GX be TopSpace; 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; 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; for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let B be Subset of X9; ( A = B implies ( A is connected iff B is connected ) )
assume A1:
A = B
; ( 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 ( not A is connected implies not B is connected )assume
not
A is
connected
;
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
;
verum end;
now ( not B is connected implies not A is connected )assume
not
B is
connected
;
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
;
verum end;
hence
( A is connected iff B is connected )
by A4; verum