let a, b be set ; :: thesis: for R being Relation st R is well-ordering & a in field R & b in field R holds
( [a,b] in R iff R -Seg a c= R -Seg b )
let R be Relation; :: thesis: ( R is well-ordering & a in field R & b in field R implies ( [a,b] in R iff R -Seg a c= R -Seg b ) )
assume that
A1: R is well-ordering and
A2: a in field R and
A3: b in field R ; :: thesis: ( [a,b] in R iff R -Seg a c= R -Seg b )
A4: R is antisymmetric by A1, Def4;
A5: R is transitive by A1, Def4;
thus ( [a,b] in R implies R -Seg a c= R -Seg b ) :: thesis: ( R -Seg a c= R -Seg b implies [a,b] in R )

proof

assume A6: [a,b] in R ; :: thesis: R -Seg a c= R -Seg b
let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in R -Seg a or c in R -Seg b )
assume A7: c in R -Seg a ; :: thesis: c in R -Seg b
then A8: [c,a] in R by Def1;
then A9: [c,b] in R by A5, A6, Lm2;
c <> a by A7, Def1;
then c <> b by A4, A6, A8, Lm3;
hence c in R -Seg b by A9, Def1; :: thesis: verum

end;

assume A10: R -Seg a c= R -Seg b ; :: thesis: [a,b] in R
A11: R is connected by A1, Def4;

A12: now

assume A13: a <> b ; :: thesis: [a,b] in R
assume not [a,b] in R ; :: thesis: contradiction
then [b,a] in R by A2, A3, A11, A13, Lm4;
then b in R -Seg a by A13, Def1;
hence contradiction by A10, Def1; :: thesis: verum

end;

R is reflexive by A1, Def4;
hence [a,b] in R by A2, A12, Lm1; :: thesis: verum