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