take STC N ; :: thesis: ( STC N is relocable & STC N is IC-recognized & STC N is proper-halt )
thus ( STC N is relocable & STC N is IC-recognized & STC N is proper-halt ) ; :: thesis: verum