let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is reflexive & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltai <> {}
let A be Subset of FT; :: thesis: ( FT is reflexive & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltai <> {} )
assume that
A1: ( FT is reflexive & FT is symmetric ) and
A2: FT is connected and
A3: A <> {} and
A4: A ` <> {} ; :: thesis: A ^deltai <> {}
A5: {} = {} FT ;
A \/ (A ` ) = [#] FT by XBOOLE_1:45;
then A6: not A,A ` are_separated by A2, A3, A4, A5, Th5, XBOOLE_1:79;

A7: now

assume A ^b meets A ` ; :: thesis: A ^deltai <> {}
then consider x being set such that
A8: ( x in A ^b & x in A ` ) by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
U_FT x meets A by A8, FIN_TOPO:13;
then consider y being set such that
A9: ( y in U_FT x & y in A ) by XBOOLE_0:3;
reconsider y = y as Element of FT by A9;
A10: x in U_FT y by A1, A9, FIN_TOPO:def 15;
y in U_FT y by A1, FIN_TOPO:def 4;
then A11: U_FT y meets A by A9, XBOOLE_0:3;
U_FT y meets A ` by A8, A10, XBOOLE_0:3;
then y in A ^delta by A11;
hence A ^deltai <> {} by A9, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume A meets (A ` ) ^b ; :: thesis: A ^deltai <> {}
then consider x being set such that
A12: ( x in (A ` ) ^b & x in A ) by XBOOLE_0:3;
reconsider x = x as Element of FT by A12;
A13: U_FT x meets A ` by A12, FIN_TOPO:13;
x in U_FT x by A1, FIN_TOPO:def 4;
then U_FT x meets A by A12, XBOOLE_0:3;
then x in A ^delta by A13;
hence A ^deltai <> {} by A12, XBOOLE_0:def 4; :: thesis: verum

end;

hence A ^deltai <> {} by A6, A7, FINTOPO4:def 1; :: thesis: verum