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