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