for X being set holds
not for x being set holds
( x in X iff x is Ordinal )