take +infty ; :: thesis: ( not +infty is real & +infty is positive )
thus ( not +infty is real & +infty is positive ) ; :: thesis: verum