let FT be non empty RelStr ; :: thesis: for X9 being non empty SubSpace of FT
for P1, Q1 being Subset of FT
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let X9 be non empty SubSpace of FT; :: thesis: for P1, Q1 being Subset of FT
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 FT; :: 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 A1: ( P = P1 & Q = Q1 ) ; :: thesis: ( not P,Q are_separated or P1,Q1 are_separated )
reconsider P2 = P, Q2 = Q as Subset of FT by Th9;
assume A2: P,Q are_separated ; :: thesis: P1,Q1 are_separated
then P ^b misses Q by FINTOPO4:def 1;
then A3: (P ^b) /\ Q = {} ;
P misses Q ^b by A2, FINTOPO4:def 1;
then A4: P /\ (Q ^b) = {} ;
P /\ (Q ^b) = P /\ (([#] X9) /\ (Q2 ^b)) by Th12
.= (P /\ ([#] X9)) /\ (Q2 ^b) by XBOOLE_1:16
.= P2 /\ (Q2 ^b) by XBOOLE_1:28 ;
then A5: P2 misses Q2 ^b by A4;
(P ^b) /\ Q = ((P2 ^b) /\ ([#] X9)) /\ Q by Th12
.= (P2 ^b) /\ (Q /\ ([#] X9)) by XBOOLE_1:16
.= (P2 ^b) /\ Q2 by XBOOLE_1:28 ;
then P2 ^b misses Q2 by A3;
hence P1,Q1 are_separated by A1, A5, FINTOPO4:def 1; :: thesis: verum