take STC N ; :: thesis: ( STC N is relocable1 & STC N is relocable2 )
thus ( STC N is relocable1 & STC N is relocable2 ) ; :: thesis: verum