let f be Function; ( f is segmental implies for a, b, c being Ordinal st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f )
given x, y being Ordinal such that A1:
dom f = x \ y
; EXCHSORT:def 1 for a, b, c being Ordinal st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f
let a, b, c be Ordinal; ( a c= b & b c= c & a in dom f & c in dom f implies b in dom f )
assume A2:
( a c= b & b c= c & a in dom f & c in dom f )
; b in dom f
then
( y c= a & c in x )
by A1, ORDINAL6:5;
then
( y c= b & b in x )
by A2, ORDINAL1:12;
hence
b in dom f
by A1, ORDINAL6:5; verum