set eq = EqRelOf A;
take EqRelOf A ; :: thesis: EqRelOf A is EqRelOf-like
thus EqRelOf A is EqRelOf-like ; :: thesis: verum