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 & B is closed ) and
A2: A misses B ; :: thesis: A,B are_separated
A /\ B = {} by A2, XBOOLE_0:def 7;
then ( (A ^b ) /\ B = {} & A /\ (B ^b ) = {} ) by A1, FIN_TOPO:def 17;
then ( A ^b misses B & A misses B ^b ) by XBOOLE_0:def 7;
hence A,B are_separated by FINTOPO4:def 1; :: thesis: verum