The prose is correct.
replyYou (presumably) aren't your grandmother, so we have x=/=y. Therefore by the biimplication, (x ≤ y and y ≤ x) is false i.e. either x ≤ y (I am better than my grandmother) or y ≤ x (my grandmother is better than me). The "neither" case is excluded by the law of totality.
> The "neither" case is excluded by the law of totality.
replyWe literally said the same thing. It doesn't follow from antisymmetry.
My point is precisely that:
(x <= y /\ y <= x) -> x = y
does not entail
x <= y \/ y <= x
The second statement is totality/comparability, not antisymmetry.