let
k
be
Nat
;
:: thesis:
k
-SD_Sub_S
c=
INT
let
e
be
object
;
:: according to
TARSKI:def 3
:: thesis:
( not
e
in
k
-SD_Sub_S
or
e
in
INT
)
assume
A1
:
e
in
k
-SD_Sub_S
;
:: thesis:
e
in
INT
k
-SD_Sub_S
c=
k
-SD_Sub
by
Th2
;
then
e
is
Integer
by
A1
,
Th8
;
hence
e
in
INT
by
INT_1:def 2
;
:: thesis:
verum