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