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