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