set IT = STC N;
set Ok = the Object-Kind of (STC N);
A1: 0 in {0} by TARSKI:def 1;
the Object-Kind of (STC N) . 0 = (0 .--> NAT) . 0 by Def11
.= NAT by A1, FUNCOP_1:7 ;
then ObjectKind (IC ) = NAT by Def11;
hence STC N is IC-Ins-separated by MEMSTR_0:def 3; :: thesis: verum