let f be Function; :: thesis: ( f is segmental implies for a, b, c being ordinal number 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 Z0: dom f = x \ y ; :: according to EXCHSORT:def 1 :: thesis: for a, b, c being ordinal number 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 number ; :: thesis: ( a c= b & b c= c & a in dom f & c in dom f implies b in dom f )
assume Z1: ( 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 Z0, ORDINAL6:5;
then ( y c= b & b in x ) by Z1, ORDINAL1:12, XBOOLE_1:1;
hence b in dom f by Z0, ORDINAL6:5; :: thesis: verum