consider f being Function such that
A1: dom f = {{}} and
A2: rng f = {{{}}} by Th5;
take f ; :: thesis: ( f is non-empty & not f is empty )
not {} in rng f by A2, TARSKI:def 1;
hence f is non-empty ; :: thesis: not f is empty
thus not f is empty by A1; :: thesis: verum