reconsider
a
=
a
,
b
=
b
as
Element
of
NAT
by
ORDINAL1:def 12
;
[
a
,
b
]
is
Element
of
[:
NAT
,
NAT
:]
;
hence
[
a
,
b
]
is
Element
of
[:
NAT
,
NAT
:]
;
:: thesis:
verum