take
STC
N
;
:: thesis:
(
STC
N
is
standard
&
STC
N
is
halting
)
thus
(
STC
N
is
standard
&
STC
N
is
halting
) ;
:: thesis:
verum