let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is reflexive & FT is connected & A <> {} & A ` <> {} holds
A ^delta <> {}
let A be Subset of FT; :: thesis: ( FT is reflexive & FT is connected & A <> {} & A ` <> {} implies A ^delta <> {} )
assume that
A1: ( FT is reflexive & FT is connected ) and
A2: ( A <> {} & A ` <> {} ) ; :: thesis: A ^delta <> {}

A3: now

assume A ^b meets A ` ; :: thesis: ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` )
then consider x being set such that
A4: x in A ^b and
A5: x in A ` by XBOOLE_0:3;
reconsider x = x as Element of FT by A4;
x in U_FT x by A1, FIN_TOPO:def 4;
then A6: U_FT x meets A ` by A5, XBOOLE_0:3;
U_FT x meets A by A4, FIN_TOPO:13;
hence ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) by A6; :: thesis: verum

end;

A7: now

assume A meets (A ` ) ^b ; :: thesis: ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` )
then consider x being set such that
A8: x in (A ` ) ^b and
A9: x in A by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
x in U_FT x by A1, FIN_TOPO:def 4;
then A10: U_FT x meets A by A9, XBOOLE_0:3;
U_FT x meets A ` by A8, FIN_TOPO:13;
hence ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) by A10; :: thesis: verum

end;

( {} = {} FT & A \/ (A ` ) = [#] FT ) by XBOOLE_1:45;
then not A,A ` are_separated by A1, A2, Th5, XBOOLE_1:79;
hence A ^delta <> {} by A3, A7, FINTOPO4:def 1, FIN_TOPO:10; :: thesis: verum