let TM be metrizable TopSpace; :: thesis: for Am, Bm being Subset of st Am,Bm are_separated holds
ex L being Subset of st L separates Am,Bm
let Am, Bm be Subset of ; :: thesis: ( Am,Bm are_separated implies ex L being Subset of st L separates Am,Bm )
assume Am,Bm are_separated ; :: thesis: ex L being Subset of st L separates Am,Bm
then consider U, W being open Subset of such that
A1: ( Am c= U & Bm c= W & U misses W ) by Lm13;
take L = (U \/ W) ` ; :: thesis: L separates Am,Bm
thus L separates Am,Bm by A1, Def3; :: thesis: verum