:: deftheorem defines separates METRIZTS:def 3 :
for T being TopSpace
for A, B, L being Subset of T holds
( L separates A,B iff ex U, W being open Subset of T st
( A c= U & B c= W & U misses W & L = (U \/ W) ` ) );