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

R -Seg a,R -Seg b are_c=-comparable

let R be Relation; :: thesis: ( R is well-ordering implies R -Seg a,R -Seg b are_c=-comparable )

assume A1: R is well-ordering ; :: thesis: R -Seg a,R -Seg b are_c=-comparable

R -Seg a,R -Seg b are_c=-comparable

let R be Relation; :: thesis: ( R is well-ordering implies R -Seg a,R -Seg b are_c=-comparable )

assume A1: R is well-ordering ; :: thesis: R -Seg a,R -Seg b are_c=-comparable

A2: now :: thesis: ( a in field R & b in field R implies R -Seg a,R -Seg b are_c=-comparable )

assume A3:
( a in field R & b in field R )
; :: thesis: R -Seg a,R -Seg b are_c=-comparable

end;now :: thesis: ( a <> b implies R -Seg a,R -Seg b are_c=-comparable )

hence
R -Seg a,R -Seg b are_c=-comparable
; :: thesis: verumassume
a <> b
; :: thesis: R -Seg a,R -Seg b are_c=-comparable

end;A4: now :: thesis: ( [b,a] in R implies R -Seg b c= R -Seg a )

assume A5:
[b,a] in R
; :: thesis: R -Seg b c= R -Seg a

end;now :: thesis: for c being object st c in R -Seg b holds

c in R -Seg a

hence
R -Seg b c= R -Seg a
; :: thesis: verumc in R -Seg a

let c be object ; :: thesis: ( c in R -Seg b implies c in R -Seg a )

assume A6: c in R -Seg b ; :: thesis: c in R -Seg a

then A7: [c,b] in R by Th1;

then A8: [c,a] in R by A1, A5, Lm2;

c <> b by A6, Th1;

then c <> a by A1, A5, A7, Lm3;

hence c in R -Seg a by A8, Th1; :: thesis: verum

end;assume A6: c in R -Seg b ; :: thesis: c in R -Seg a

then A7: [c,b] in R by Th1;

then A8: [c,a] in R by A1, A5, Lm2;

c <> b by A6, Th1;

then c <> a by A1, A5, A7, Lm3;

hence c in R -Seg a by A8, Th1; :: thesis: verum

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

hence
R -Seg a,R -Seg b are_c=-comparable
by A1, A3, A4, Lm4; :: thesis: verumassume A9:
[a,b] in R
; :: thesis: R -Seg a c= R -Seg b

end;now :: thesis: for c being object st c in R -Seg a holds

c in R -Seg b

hence
R -Seg a c= R -Seg b
; :: thesis: verumc in R -Seg b

let c be object ; :: thesis: ( c in R -Seg a implies c in R -Seg b )

assume A10: c in R -Seg a ; :: thesis: c in R -Seg b

then A11: [c,a] in R by Th1;

then A12: [c,b] in R by A1, A9, Lm2;

c <> a by A10, Th1;

then c <> b by A1, A9, A11, Lm3;

hence c in R -Seg b by A12, Th1; :: thesis: verum

end;assume A10: c in R -Seg a ; :: thesis: c in R -Seg b

then A11: [c,a] in R by Th1;

then A12: [c,b] in R by A1, A9, Lm2;

c <> a by A10, Th1;

then c <> b by A1, A9, A11, Lm3;

hence c in R -Seg b by A12, Th1; :: thesis: verum

now :: thesis: ( ( R -Seg a = {} or R -Seg b = {} ) implies R -Seg a,R -Seg b are_c=-comparable )

hence
R -Seg a,R -Seg b are_c=-comparable
by A2, Th2; :: thesis: verumassume
( R -Seg a = {} or R -Seg b = {} )
; :: thesis: R -Seg a,R -Seg b are_c=-comparable

then ( R -Seg a c= R -Seg b or R -Seg b c= R -Seg a ) ;

hence R -Seg a,R -Seg b are_c=-comparable ; :: thesis: verum

end;then ( R -Seg a c= R -Seg b or R -Seg b c= R -Seg a ) ;

hence R -Seg a,R -Seg b are_c=-comparable ; :: thesis: verum