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

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 )

( [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 )

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 A8:
R -Seg a c= R -Seg b
; :: thesis: [a,b] in R
assume A4:
[a,b] in R
; :: thesis: R -Seg a c= R -Seg b

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in R -Seg a or c in R -Seg b )

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

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

then A7: [c,b] in R by A1, A4, Lm2;

c <> a by A5, Th1;

then c <> b by A1, A4, A6, Lm3;

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

end;let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in R -Seg a or c in R -Seg b )

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

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

then A7: [c,b] in R by A1, A4, Lm2;

c <> a by A5, Th1;

then c <> b by A1, A4, A6, Lm3;

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

now :: thesis: ( a <> b implies [a,b] in R )

hence
[a,b] in R
by A1, A2, Lm1; :: thesis: verumassume A9:
a <> b
; :: thesis: [a,b] in R

assume not [a,b] in R ; :: thesis: contradiction

then [b,a] in R by A2, A3, A1, A9, Lm4;

then b in R -Seg a by A9, Th1;

hence contradiction by A8, Th1; :: thesis: verum

end;assume not [a,b] in R ; :: thesis: contradiction

then [b,a] in R by A2, A3, A1, A9, Lm4;

then b in R -Seg a by A9, Th1;

hence contradiction by A8, Th1; :: thesis: verum