let FT be non empty RelStr ; for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds
A,B are_separated
let A, B be Subset of FT; ( FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A implies A,B are_separated )
assume that
A1:
FT is filled
and
A2:
A /\ B = {}
and
A3:
(A ^deltao) /\ B = {}
and
A4:
(B ^deltao) /\ A = {}
; XBOOLE_0:def 7 A,B are_separated
(B `) /\ ((B ^delta) /\ A) = {}
by A4, XBOOLE_1:16;
then
(B `) /\ (((B ^b) /\ ((B `) ^b)) /\ A) = {}
by FIN_TOPO:18;
then
(B `) /\ (((B `) ^b) /\ ((B ^b) /\ A)) = {}
by XBOOLE_1:16;
then A5:
((B `) /\ ((B `) ^b)) /\ ((B ^b) /\ A) = {}
by XBOOLE_1:16;
(B `) /\ ((B `) ^b) = B `
by A1, FIN_TOPO:13, XBOOLE_1:28;
then
B ` misses (B ^b) /\ A
by A5;
then
(B ^b) /\ A c= B
by SUBSET_1:24;
then
((B ^b) /\ A) /\ A c= B /\ A
by XBOOLE_1:26;
then
(B ^b) /\ (A /\ A) c= B /\ A
by XBOOLE_1:16;
then
(B ^b) /\ A = {}
by A2, XBOOLE_1:3;
then A6:
A misses B ^b
;
(A `) /\ ((A ^delta) /\ B) = {}
by A3, XBOOLE_1:16;
then
(A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) = {}
by FIN_TOPO:18;
then
(A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) = {}
by XBOOLE_1:16;
then A7:
((A `) /\ ((A `) ^b)) /\ ((A ^b) /\ B) = {}
by XBOOLE_1:16;
(A `) /\ ((A `) ^b) = A `
by A1, FIN_TOPO:13, XBOOLE_1:28;
then
A ` misses (A ^b) /\ B
by A7;
then
(A ^b) /\ B c= A
by SUBSET_1:24;
then
((A ^b) /\ B) /\ B c= A /\ B
by XBOOLE_1:26;
then
(A ^b) /\ (B /\ B) c= A /\ B
by XBOOLE_1:16;
then
(A ^b) /\ B = {}
by A2, XBOOLE_1:3;
then
A ^b misses B
;
hence
A,B are_separated
by A6, FINTOPO4:def 1; verum