take -infty ; :: thesis: -infty is -Inf-like
thus -infty is -Inf-like by Def4; :: thesis: verum