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