theorem :: ORDINAL1:27

for X being set ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )