theorem Th25: :: TOPS_2:25

for T being TopStruct
for Q being Subset of T
for A being SubSpace of T st Q is open holds
for P being Subset of A st P = Q holds
P is open