The `Subset` example in the Syntax chapter is outdated

I am using Lean 4.25.2. The Syntax chapter contains:

```
instance : Subset (Set α) where
  subset X Y := ∀ (x : α), x ∈ X → x ∈ Y
```

The class `Subset` seems to have been renamed to `HasSubset`, and `subset` to `Subset`. The following works with the current stable Lean version:

```
instance : HasSubset (Set α) where
  Subset X Y := ∀ (x : α), x ∈ X → x ∈ Y
```
