let
n
be
Nat
;
:: thesis:
square-uparrow
n
=
[:
(
NAT
\
(
Segm
n
)
)
,
(
NAT
\
(
Segm
n
)
)
:]
reconsider
no
=
n
as
Element
of
OrderedNAT
by
ORDINAL1:def 12
;
uparrow
no
=
NAT
\
(
Segm
n
)
by
Th13
;
hence
square-uparrow
n
=
[:
(
NAT
\
(
Segm
n
)
)
,
(
NAT
\
(
Segm
n
)
)
:]
by
Th26
;
:: thesis:
verum