let
x
be
object
;
:: according to
TARSKI:def 3
:: thesis:
( not
x
in
{
REAL
}
or
x
in
the
carrier
of
REAL?
)
assume
x
in
{
REAL
}
;
:: thesis:
x
in
the
carrier
of
REAL?
then
x
in
(
REAL
\
NAT
)
\/
{
REAL
}
by
XBOOLE_0:def 3
;
hence
x
in
the
carrier
of
REAL?
by
Def8
;
:: thesis:
verum