take STC N ; :: thesis: STC N is relocable1
thus STC N is relocable1 ; :: thesis: verum