theorem :: TSEP_1:3
for X being strict TopStruct holds X | ([#] X) = X