let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st A is closed & B is closed & A misses B holds
A,B are_separated
let A, B be Subset of FT; :: thesis: ( A is closed & B is closed & A misses B implies A,B are_separated )
assume that
A1: A is closed and
A2: B is closed and
A3: A misses B ; :: thesis: A,B are_separated
A4: A /\ B = {} by A3, XBOOLE_0:def 7;
then A /\ (B ^b) = {} by A2, FIN_TOPO:def 15;
then A5: A misses B ^b by XBOOLE_0:def 7;
(A ^b) /\ B = {} by A1, A4, FIN_TOPO:def 15;
then A ^b misses B by XBOOLE_0:def 7;
hence A,B are_separated by A5, FINTOPO4:def 1; :: thesis: verum