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