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