let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltai <> {}

let A be Subset of FT; :: thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltai <> {} )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: ( FT is connected & A <> {} & A ` <> {} ) ; :: thesis:
A3: now :: thesis: ( A ^b meets A ` implies A ^deltai <> {} )
assume A ^b meets A ` ; :: thesis:
then consider x being object 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;
U_FT x meets A by ;
then consider y being object such that
A6: y in U_FT x and
A7: y in A by XBOOLE_0:3;
reconsider y = y as Element of FT by A6;
y in U_FT y by A1;
then A8: U_FT y meets A by ;
x in U_FT y by A1, A6;
then U_FT y meets A ` by ;
then y in A ^delta by A8;
hence A ^deltai <> {} by ; :: thesis: verum
end;
A9: now :: thesis: ( A meets (A `) ^b implies A ^deltai <> {} )
assume A meets (A `) ^b ; :: thesis:
then consider x being object such that
A10: x in (A `) ^b and
A11: x in A by XBOOLE_0:3;
reconsider x = x as Element of FT by A10;
x in U_FT x by A1;
then A12: U_FT x meets A by ;
U_FT x meets A ` by ;
then x in A ^delta by A12;
hence A ^deltai <> {} by ; :: thesis: verum
end;
( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45;
then not A,A ` are_separated by ;
hence A ^deltai <> {} by ; :: thesis: verum