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

let A be Subset of FT; :: thesis: ( FT is filled & FT is connected & A <> {} & A ` <> {} implies A ^delta <> {} )
assume that
A1: ( FT is filled & FT is connected ) and
A2: ( A <> {} & A ` <> {} ) ; :: thesis:
A3: now :: thesis: ( A ^b meets A ` implies ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) )
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 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;
x in U_FT x by A1;
then A6: U_FT x meets A ` by ;
U_FT x meets A by ;
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 :: thesis: ( A meets (A `) ^b implies ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) )
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 object 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;
then A10: U_FT x meets A by ;
U_FT x meets A ` by ;
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 ;
hence A ^delta <> {} by ; :: thesis: verum