let GX be TopSpace; :: thesis: for X9 being SubSpace of GX

for P1, Q1 being Subset of GX

for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let X9 be SubSpace of GX; :: thesis: for P1, Q1 being Subset of GX

for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let P1, Q1 be Subset of GX; :: thesis: for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let P, Q be Subset of X9; :: thesis: ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated )

assume that

A1: P = P1 and

A2: Q = Q1 ; :: thesis: ( not P,Q are_separated or P1,Q1 are_separated )

reconsider P2 = P, Q2 = Q as Subset of GX by PRE_TOPC:11;

assume that

A3: (Cl P) /\ Q = {} and

A4: P /\ (Cl Q) = {} ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: P1,Q1 are_separated

P /\ (Cl Q) = P /\ (([#] X9) /\ (Cl Q2)) by PRE_TOPC:17

.= (P /\ ([#] X9)) /\ (Cl Q2) by XBOOLE_1:16

.= P2 /\ (Cl Q2) by XBOOLE_1:28 ;

then A5: P2 misses Cl Q2 by A4;

(Cl P) /\ Q = ((Cl P2) /\ ([#] X9)) /\ Q by PRE_TOPC:17

.= (Cl P2) /\ (Q /\ ([#] X9)) by XBOOLE_1:16

.= (Cl P2) /\ Q2 by XBOOLE_1:28 ;

then Cl P2 misses Q2 by A3;

hence P1,Q1 are_separated by A1, A2, A5; :: thesis: verum

for P1, Q1 being Subset of GX

for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let X9 be SubSpace of GX; :: thesis: for P1, Q1 being Subset of GX

for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let P1, Q1 be Subset of GX; :: thesis: for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds

P1,Q1 are_separated

let P, Q be Subset of X9; :: thesis: ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated )

assume that

A1: P = P1 and

A2: Q = Q1 ; :: thesis: ( not P,Q are_separated or P1,Q1 are_separated )

reconsider P2 = P, Q2 = Q as Subset of GX by PRE_TOPC:11;

assume that

A3: (Cl P) /\ Q = {} and

A4: P /\ (Cl Q) = {} ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: P1,Q1 are_separated

P /\ (Cl Q) = P /\ (([#] X9) /\ (Cl Q2)) by PRE_TOPC:17

.= (P /\ ([#] X9)) /\ (Cl Q2) by XBOOLE_1:16

.= P2 /\ (Cl Q2) by XBOOLE_1:28 ;

then A5: P2 misses Cl Q2 by A4;

(Cl P) /\ Q = ((Cl P2) /\ ([#] X9)) /\ Q by PRE_TOPC:17

.= (Cl P2) /\ (Q /\ ([#] X9)) by XBOOLE_1:16

.= (Cl P2) /\ Q2 by XBOOLE_1:28 ;

then Cl P2 misses Q2 by A3;

hence P1,Q1 are_separated by A1, A2, A5; :: thesis: verum