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 ^deltao <> {}

let A be Subset of FT; :: thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltao <> {} )

assume that

A1: ( FT is filled & FT is symmetric ) and

A2: ( FT is connected & A <> {} & A ` <> {} ) ; :: thesis: A ^deltao <> {}

then not A,A ` are_separated by A2, Th4, XBOOLE_1:79;

hence A ^deltao <> {} by A9, A3, FINTOPO4:def 1; :: thesis: verum

A ^deltao <> {}

let A be Subset of FT; :: thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltao <> {} )

assume that

A1: ( FT is filled & FT is symmetric ) and

A2: ( FT is connected & A <> {} & A ` <> {} ) ; :: thesis: A ^deltao <> {}

A3: now :: thesis: ( A meets (A `) ^b implies A ^deltao <> {} )

assume
A meets (A `) ^b
; :: thesis: A ^deltao <> {}

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 A4, FIN_TOPO:8;

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 A7, XBOOLE_0:3;

x in U_FT y by A1, A6;

then U_FT y meets A by A5, XBOOLE_0:3;

then y in A ^delta by A8;

hence A ^deltao <> {} by A7, XBOOLE_0:def 4; :: thesis: verum

end;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 A4, FIN_TOPO:8;

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 A7, XBOOLE_0:3;

x in U_FT y by A1, A6;

then U_FT y meets A by A5, XBOOLE_0:3;

then y in A ^delta by A8;

hence A ^deltao <> {} by A7, XBOOLE_0:def 4; :: thesis: verum

A9: now :: thesis: ( A ^b meets A ` implies A ^deltao <> {} )

( {} = {} FT & A \/ (A `) = [#] FT )
by XBOOLE_1:45;assume
A ^b meets A `
; :: thesis: A ^deltao <> {}

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 A11, XBOOLE_0:3;

U_FT x meets A by A10, FIN_TOPO:8;

then x in A ^delta by A12;

hence A ^deltao <> {} by A11, XBOOLE_0:def 4; :: thesis: verum

end;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 A11, XBOOLE_0:3;

U_FT x meets A by A10, FIN_TOPO:8;

then x in A ^delta by A12;

hence A ^deltao <> {} by A11, XBOOLE_0:def 4; :: thesis: verum

then not A,A ` are_separated by A2, Th4, XBOOLE_1:79;

hence A ^deltao <> {} by A9, A3, FINTOPO4:def 1; :: thesis: verum