let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st FT is reflexive & [#] FT = A \/ B & A,B are_separated holds
( A is open & A is closed )
let A, B be Subset of FT; :: thesis: ( FT is reflexive & [#] FT = A \/ B & A,B are_separated implies ( A is open & A is closed ) )
assume that
A1: FT is reflexive and
A2: [#] FT = A \/ B and
A3: A,B are_separated ; :: thesis: ( A is open & A is closed )
A4: B c= B ^b by A1, FIN_TOPO:18;

now

assume A misses B ^b ; :: thesis: B ^b = B
then B ^b c= B by A2, XBOOLE_1:73;
hence B ^b = B by A4, XBOOLE_0:def 10; :: thesis: verum

end;

then A5: B is closed by A3, FINTOPO4:def 1, FIN_TOPO:def 17;
A6: A c= A ^b by A1, FIN_TOPO:18;

A7: now

assume A ^b misses B ; :: thesis: A ^b = A
then A ^b c= A by A2, XBOOLE_1:73;
hence A ^b = A by A6, XBOOLE_0:def 10; :: thesis: verum

end;

B ` = A by A1, A2, A3, FINTOPO4:6, PRE_TOPC:25;
hence ( A is open & A is closed ) by A3, A7, A5, FINTOPO4:def 1, FIN_TOPO:31, FIN_TOPO:def 17; :: thesis: verum