let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds

( A is open & A is closed )

let A, B be Subset of FT; :: thesis: ( FT is filled & [#] FT = A \/ B & A,B are_separated implies ( A is open & A is closed ) )

assume that

A1: FT is filled and

A2: [#] FT = A \/ B and

A3: A,B are_separated ; :: thesis: ( A is open & A is closed )

B c= B ^b by A1, FIN_TOPO:13;

then ( A misses B ^b implies B ^b = B ) by A2, XBOOLE_1:73;

then A4: B is closed by A3, FINTOPO4:def 1;

A c= A ^b by A1, FIN_TOPO:13;

then A5: ( A ^b misses B implies A ^b = A ) by A2, XBOOLE_1:73;

B ` = A by A1, A2, A3, FINTOPO4:6, PRE_TOPC:5;

hence ( A is open & A is closed ) by A3, A5, A4, FINTOPO4:def 1, FIN_TOPO:24; :: thesis: verum

( A is open & A is closed )

let A, B be Subset of FT; :: thesis: ( FT is filled & [#] FT = A \/ B & A,B are_separated implies ( A is open & A is closed ) )

assume that

A1: FT is filled and

A2: [#] FT = A \/ B and

A3: A,B are_separated ; :: thesis: ( A is open & A is closed )

B c= B ^b by A1, FIN_TOPO:13;

then ( A misses B ^b implies B ^b = B ) by A2, XBOOLE_1:73;

then A4: B is closed by A3, FINTOPO4:def 1;

A c= A ^b by A1, FIN_TOPO:13;

then A5: ( A ^b misses B implies A ^b = A ) by A2, XBOOLE_1:73;

B ` = A by A1, A2, A3, FINTOPO4:6, PRE_TOPC:5;

hence ( A is open & A is closed ) by A3, A5, A4, FINTOPO4:def 1, FIN_TOPO:24; :: thesis: verum