ex x1, x2 being set st the Element of f = [x1,x2] by Def1;
hence not rng f is empty by Def5; :: thesis: verum