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