let
n
,
k
be
Nat
;
:: thesis:
for
a
being non
trivial
Nat
st
Px
(
a
,
k
)
=
Px
(
a
,
n
) holds
k
=
n
let
a
be non
trivial
Nat
;
:: thesis:
(
Px
(
a
,
k
)
=
Px
(
a
,
n
) implies
k
=
n
)
(
k
<
n
or
n
<
k
or
k
=
n
)
by
XXREAL_0:1
;
hence
(
Px
(
a
,
k
)
=
Px
(
a
,
n
) implies
k
=
n
)
by
Th19
;
:: thesis:
verum