reconsider
f
=
{}
as
PartFunc
of
REAL
,
REAL
by
RELSET_1:12
;
take
f
;
:: thesis:
f
is
trivial
thus
f
is
trivial
;
:: thesis:
verum