let TS be TopSpace; :: thesis: {} TS is open
Int ({} TS) = {} TS ;
hence {} TS is open ; :: thesis: verum