take STC N ; :: thesis: ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated & STC N is definite )
thus ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated & STC N is definite ) ; :: thesis: verum