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