take <%> REAL ; :: thesis: <%> REAL is non-zero
thus <%> REAL is non-zero ; :: thesis: verum