let TM be metrizable TopSpace; 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; ( Am,Bm are_separated implies ex L being Subset of TM st L separates Am,Bm )
assume
Am,Bm are_separated
; 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 Lm13;
take
(U \/ W) `
; (U \/ W) ` separates Am,Bm
thus
(U \/ W) ` separates Am,Bm
by A1; verum