let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st FT is reflexive & 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 reflexive & A misses B & A ^deltao misses B & B ^deltao misses A implies A,B are_separated )
assume that
A1: FT is reflexive 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:24;
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:18, XBOOLE_1:28;
then B ` misses (B ^b ) /\ A by A5, XBOOLE_0:def 7;
then (B ^b ) /\ A c= B by SUBSET_1:44;
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 by XBOOLE_0:def 7;
(A ` ) /\ ((A ^delta ) /\ B) = {} by A3, XBOOLE_1:16;
then (A ` ) /\ (((A ^b ) /\ ((A ` ) ^b )) /\ B) = {} by FIN_TOPO:24;
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:18, XBOOLE_1:28;
then A ` misses (A ^b ) /\ B by A7, XBOOLE_0:def 7;
then (A ^b ) /\ B c= A by SUBSET_1:44;
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 by XBOOLE_0:def 7;
hence A,B are_separated by A6, FINTOPO4:def 1; :: thesis: verum