:: deftheorem Def3 defines sup ORDINAL2:def 3 :
for X being set
for b₂ being Ordinal holds
( b₂ = sup X iff ( On X c= b₂ & ( for A being Ordinal st On X c= A holds
b₂ c= A ) ) );