let
x
be
Element
of
R
;
:: thesis:
x
is
real
the
carrier
of
R
c=
REAL
by
Def1
;
hence
x
is
real
;
:: thesis:
verum