let a, b be set ; :: 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 )

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, Th37;
hence ( a = b or a in R -Seg b ) by Def1; :: thesis: verum

end;

now

assume a in R -Seg b ; :: thesis: R -Seg a c= R -Seg b
then [a,b] in R by Def1;
hence R -Seg a c= R -Seg b by A1, Th37; :: thesis: verum

end;

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