for X being set holds
( X is ordinal-membered iff On X = X )