let f be Function; :: thesis: ( 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 ; :: according to EXCHSORT:def 1 :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum