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: A ^delta <> {}

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

hence A ^delta <> {} by A3, A7, FINTOPO4:def 1, FIN_TOPO:5; :: thesis: verum

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: A ^delta <> {}

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 ` ) )

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

U_FT x meets A by A4, FIN_TOPO:8;

hence ex z being Element of FT st

( U_FT z meets A & U_FT z meets A ` ) by A6; :: thesis: verum

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

U_FT x meets A by A4, FIN_TOPO:8;

hence ex z being Element of FT st

( U_FT z meets A & U_FT z meets A ` ) by A6; :: thesis: verum

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 ` ) )

( {} = {} FT & A \/ (A `) = [#] FT )
by XBOOLE_1:45;( 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 A9, XBOOLE_0:3;

U_FT x meets A ` by A8, FIN_TOPO:8;

hence ex z being Element of FT st

( U_FT z meets A & U_FT z meets A ` ) by A10; :: thesis: verum

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

U_FT x meets A ` by A8, FIN_TOPO:8;

hence ex z being Element of FT st

( U_FT z meets A & U_FT z meets A ` ) by A10; :: thesis: verum

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

hence A ^delta <> {} by A3, A7, FINTOPO4:def 1, FIN_TOPO:5; :: thesis: verum