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;

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;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

now :: thesis: ( not B is connected implies not A is connected )

hence
( A is connected iff B is connected )
by A4; :: thesis: verumassume
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;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