theorem :: PBOOLE:1

for f being Function st f is non-empty holds
rng f is with_non-empty_elements ;