theorem :: METRIZTS:10

for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds
F is F_sigma