let FT be non empty RelStr ; :: thesis: 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; :: thesis: ( 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 = {} ; :: according to XBOOLE_0:def 7 :: thesis: 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; :: thesis: verum