theorem :: FINTOPO8:9

for NT being NTopSpace
for A being Subset of NT holds Int A = union { O where O is open Subset of NT : O c= A } by Lm5;