let TS be TopSpace; :: thesis: Int ([#] TS) = [#] TS
Int ([#] TS) = ({} TS) ` by PRE_TOPC:22;
hence Int ([#] TS) = [#] TS ; :: thesis: verum