(
0
<=
f
.
x
&
f
.
x
<=
1 )
by
FUZZY_2:1
;
then
f
.
x
in
[.
0
,1
.]
by
XXREAL_1:1
;
hence
f
.
x
is
Element
of
(
RealPoset
[.
0
,1
.]
)
by
Def3
;
:: thesis:
verum