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

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

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