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 & [#] FT = A \/ B ) and
A2: A,B are_separated ; :: thesis: ( A is open & A is closed )
A3: ( A c= A ^b & B c= B ^b ) by A1, FIN_TOPO:18;

A4: now

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

end;

now

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

end;

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