take f = {{} } --> {} ; :: thesis: ( not f is empty & f is constant )
thus ( not f is empty & f is constant ) ; :: thesis: verum