let FT be non empty filled RelStr ; :: thesis: for A, B being Subset of FT st A,B are_separated holds
A misses B
let A, B be Subset of FT; :: thesis: ( A,B are_separated implies A misses B )
assume A,B are_separated ; :: thesis: A misses B
then A ^b misses B by Def1;
hence A misses B by FIN_TOPO:18, XBOOLE_1:63; :: thesis: verum