consider f being empty Function;
take f ; :: thesis: f is trivial
thus f is trivial ; :: thesis: verum