![](https://secure.gravatar.com/avatar/da56018fec1036eb1e02305d09a0bce8.jpg?s=120&d=mm&r=g)
30 Sep
2011
30 Sep
'11
11:04 a.m.
that would be very useful for sets and german decimals: $x = 1,33$ vs. $x ∈ {1, 2, 3, 4}$