let FT be non empty RelStr ; 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; 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; 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; ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated )
assume A1:
( P = P1 & Q = Q1 )
; ( 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
; 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; verum