Terminals SCM-AE = [:{1},NAT:] by Def1;
then consider x, y being object such that
A1: x in {1} and
A2: y in NAT and
A3: t = [x,y] by ZFMISC_1:84;
reconsider k = y as Element of NAT by A2;
take k ; :: thesis: dl. k = t
thus dl. k = t by A1, A3, TARSKI:def 1; :: thesis: verum