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