:: deftheorem Def1 defines segmental EXCHSORT:def 1 :
for f being set holds
( f is segmental iff ex a, b being Ordinal st proj1 f = a \ b );