take {} ; :: thesis: ( {} is empty & {} is constanT )
thus ( {} is empty & {} is constanT ) ; :: thesis: verum