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