per
cases
(
k
=
0
or ex
k9
being
Nat
st
k
=
k9
+
1 )
by
NAT_1:6
;
suppose
A1
:
k
=
0
;
:: thesis:
0_
(
k
,
G
) is
Cycle
of
k
,
G
card
{}
=
2
*
0
;
hence
0_
(
k
,
G
) is
Cycle
of
k
,
G
by
A1
,
Def14
;
:: thesis:
verum
end;
suppose
ex
k9
being
Nat
st
k
=
k9
+
1 ;
:: thesis:
0_
(
k
,
G
) is
Cycle
of
k
,
G
then
consider
k9
being
Nat
such that
A2
:
k
=
k9
+
1 ;
reconsider
k9
=
k9
as
Element
of
NAT
by
ORDINAL1:def 12
;
del
(
0_
(
(
k9
+
1
)
,
G
)
)
=
0_
(
k9
,
G
)
by
Th56
;
hence
0_
(
k
,
G
) is
Cycle
of
k
,
G
by
A2
,
Def14
;
:: thesis:
verum
end;
end;