let GX be TopSpace; :: thesis: for X' being SubSpace of GX
for P, Q being Subset of GX
for P1, Q1 being Subset of X' st P = P1 & Q = Q1 & P \/ Q c= [#] X' & P,Q are_separated holds
P1,Q1 are_separated
let X' be SubSpace of GX; :: thesis: for P, Q being Subset of GX
for P1, Q1 being Subset of X' st P = P1 & Q = Q1 & P \/ Q c= [#] X' & P,Q are_separated holds
P1,Q1 are_separated
let P, Q be Subset of GX; :: thesis: for P1, Q1 being Subset of X' st P = P1 & Q = Q1 & P \/ Q c= [#] X' & P,Q are_separated holds
P1,Q1 are_separated
let P1, Q1 be Subset of X'; :: thesis: ( P = P1 & Q = Q1 & P \/ Q c= [#] X' & P,Q are_separated implies P1,Q1 are_separated )
assume that
A1: P = P1 and
A2: Q = Q1 and
A3: P \/ Q c= [#] X' ; :: thesis: ( not P,Q are_separated or P1,Q1 are_separated )
A4: Q c= P \/ Q by XBOOLE_1:7;
P c= P \/ Q by XBOOLE_1:7;
then reconsider P2 = P, Q2 = Q as Subset of X' by A3, A4, XBOOLE_1:1;
assume that
A5: (Cl P) /\ Q = {} and
A6: P /\ (Cl Q) = {} ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: P1,Q1 are_separated
P2 /\ (Cl Q2) = P2 /\ (([#] X') /\ (Cl Q)) by PRE_TOPC:47
.= (P2 /\ ([#] X')) /\ (Cl Q) by XBOOLE_1:16
.= P /\ (Cl Q) by XBOOLE_1:28 ;
then A7: P2 misses Cl Q2 by A6, XBOOLE_0:def 7;
Cl P2 = (Cl P) /\ ([#] X') by PRE_TOPC:47;
then (Cl P2) /\ Q2 = (Cl P) /\ (Q2 /\ ([#] X')) by XBOOLE_1:16
.= (Cl P) /\ Q by XBOOLE_1:28 ;
then Cl P2 misses Q2 by A5, XBOOLE_0:def 7;
hence P1,Q1 are_separated by A1, A2, A7, Def1; :: thesis: verum