:: deftheorem defines -based EXCHSORT:def 2 :
for a being Ordinal
for s being set holds
( s is a -based iff for b being Ordinal st b in proj1 s holds
( a in proj1 s & a c= b ) );