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