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

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