reconsider
ZERO
=
0
as
Integer
;
0
>
0

1 ;
then
0
'
1
=
0
by
XREAL_0:def 2
;
then
A1
:
Radix
(
0
'
1
)
=
1
by
POWER:24
;
ZERO
is
Element
of
INT
by
INT_1:def 2
;
hence
0
in
0
SD_Sub_S
by
A1
;
:: thesis:
verum