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 )
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;
now :: thesis: ( a in R -Seg b implies R -Seg a c= R -Seg b )
assume 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;
hence ( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b ) ; :: thesis: verum