theorem Th22: :: TOPS_1:22

for TS being TopSpace
for x being set
for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )