let FT be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum