Membership in the selected distance class

A point belongs to the selected distance class exactly when it belongs to the finite set and is at the selected distance from the source point.

Let $A$ be a finite subset of the Euclidean plane $\mathbb{R}^2$, let $s \in \mathbb{R}^2$ be a source point, and let $d \in \mathbb{R}$ be a target distance. The selected distance class of $A$ relative to $s$ and $d$ is the sub-collection of points of $A$ lying at distance exactly $d$ from $s$. The theorem states that a point $q\in\mathbb{R}^2$ belongs to this class if and only if it belongs to $A$ and $\operatorname{dist}(s,q)=d$:

This is the defining membership characterization for the selected distance class used throughout the formalization of Erdos problem 97/96 on isosceles-free point sets, where the selected class isolates the points of a configuration lying on a common circle centered at a witness point.

Formalization Note This is a corrected, canonical restatement of an earlier registration of the same fact whose formal statement used a local $\mathbb{R}^2$ notation abbreviation that the verification service could not resolve, causing every proof attempt against it (by multiple independent submitters) to fail with an identical parser error regardless of content. This restatement spells out \ directly and is otherwise word-for-word identical to the original.