take -infty ; :: thesis: ( not -infty is real & -infty is negative )
thus ( not -infty is real & -infty is negative ) ; :: thesis: verum