dom
r
=
the
carrier
of
F
by
defr
;
then
r
.
(
0.
F
)
<>
r
.
(
1.
F
)
by
FUNCT_1:def 4
;
then
0.
(
RenField
r
)
<>
r
.
(
1.
F
)
by
defrf
;
hence
not
RenField
r
is
degenerated
by
defrf
;
:: thesis:
verum