let FT be non empty RelStr ; 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; ( 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
; ( 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; verum