let a, b be set ; :: 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 R is well-ordering ; :: thesis: R -Seg a,R -Seg b are_c=-comparable
then A1: ( R is connected & R is transitive & R is reflexive & R is antisymmetric ) by Def4;

A2: now

assume ( 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 ) by XBOOLE_1:2;
hence R -Seg a,R -Seg b are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

now

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

now

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

A4: now

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

now

let c be set ; :: thesis: ( c in R -Seg a implies c in R -Seg b )
assume c in R -Seg a ; :: thesis: c in R -Seg b
then A6: ( [c,a] in R & c <> a ) by Def1;
then A7: [c,b] in R by A1, A5, Lm2;
c <> b by A1, A5, A6, Lm3;
hence c in R -Seg b by A7, Def1; :: thesis: verum

end;

hence R -Seg a c= R -Seg b by TARSKI:def 3; :: thesis: verum

end;

now

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

now

let c be set ; :: thesis: ( c in R -Seg b implies c in R -Seg a )
assume c in R -Seg b ; :: thesis: c in R -Seg a
then A9: ( [c,b] in R & c <> b ) by Def1;
then A10: [c,a] in R by A1, A8, Lm2;
c <> a by A1, A8, A9, Lm3;
hence c in R -Seg a by A10, Def1; :: thesis: verum

end;

hence R -Seg b c= R -Seg a by TARSKI:def 3; :: thesis: verum

end;

hence R -Seg a,R -Seg b are_c=-comparable by A1, A3, A4, Lm4, XBOOLE_0:def 9; :: thesis: verum

end;

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

end;

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