reconsider x = - 1 as set ;
take x ; :: thesis: x is dim-like
thus x is dim-like ; :: thesis: verum