take STC N ; :: thesis: ( STC N is weakly_standard & STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is standard-ins )
thus ( STC N is weakly_standard & STC N is halting & STC N is realistic & STC N is steady-programmed & STC N is standard-ins ) ; :: thesis: verum