theorem :: PRE_TOPC:6

for T being 1-sorted holds [#] T = ({} T) ` ;