take [#] X ; :: thesis: ( [#] X is open & [#] X is closed & [#] X is dense )
thus ( [#] X is open & [#] X is closed & [#] X is dense ) ; :: thesis: verum