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 A1: ( FT is reflexive & A /\ B = {} & (A ^deltao ) /\ B = {} & (B ^deltao ) /\ A = {} ) ; :: according to XBOOLE_0:def 7 :: thesis: A,B are_separated
then (A ` ) /\ ((A ^delta ) /\ B) = {} by 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 A2: ((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 A2, 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 A3: (A ^b ) /\ B = {} by A1, XBOOLE_1:3;
(B ` ) /\ ((B ^delta ) /\ A) = {} by A1, 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 A4: ((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 A4, 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 A1, XBOOLE_1:3;
then ( A ^b misses B & A misses B ^b ) by A3, XBOOLE_0:def 7;
hence A,B are_separated by FINTOPO4:def 1; :: thesis: verum