let a, b be object ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in field R holds

( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )

let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in field R implies ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) ) )

assume A1: ( R is well-ordering & a in field R & b in field R ) ; :: thesis: ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )

thus ( not R -Seg a c= R -Seg b or a = b or a in R -Seg b ) :: thesis: ( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b )

( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )

let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in field R implies ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) ) )

assume A1: ( R is well-ordering & a in field R & b in field R ) ; :: thesis: ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )

thus ( not R -Seg a c= R -Seg b or a = b or a in R -Seg b ) :: thesis: ( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b )

proof

assume
R -Seg a c= R -Seg b
; :: thesis: ( a = b or a in R -Seg b )

then [a,b] in R by A1, Th29;

hence ( a = b or a in R -Seg b ) by Th1; :: thesis: verum

end;then [a,b] in R by A1, Th29;

hence ( a = b or a in R -Seg b ) by Th1; :: thesis: verum

now :: thesis: ( a in R -Seg b implies R -Seg a c= R -Seg b )

hence
( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b )
; :: thesis: verumassume
a in R -Seg b
; :: thesis: R -Seg a c= R -Seg b

then [a,b] in R by Th1;

hence R -Seg a c= R -Seg b by A1, Th29; :: thesis: verum

end;then [a,b] in R by Th1;

hence R -Seg a c= R -Seg b by A1, Th29; :: thesis: verum