take
STC N
; :: thesis: ( STC N is relocable & STC N is IC-recognized & STC N is CurIns-recognized )

thus ( STC N is relocable & STC N is IC-recognized & STC N is CurIns-recognized ) ; :: thesis: verum

thus ( STC N is relocable & STC N is IC-recognized & STC N is CurIns-recognized ) ; :: thesis: verum