consider
d9
being
Nat
such that
A1
:
d
=
d9
+
1
by
NAT_1:6
;
reconsider
d9
=
d9
as
Element
of
NAT
by
ORDINAL1:def 12
;
reconsider
G
=
G
as
Grating
of
d9
+
1
by
A1
;
del
(
Omega
G
)
=
0_
(
d9
,
G
)
by
Th57
;
hence
Omega
G
is
Cycle
of
d
,
G
by
A1
,
Def14
;
:: thesis:
verum