for E being set holds [#] E = ({} E) ` ;