take
F
=
Stop
S
;
:: thesis:
(
F
is
really-closed
&
F
is
trivial
)
thus
(
F
is
really-closed
&
F
is
trivial
) ;
:: thesis:
verum