let L be antisymmetric RelStr ; :: thesis: for R being auxiliary(i) Relation of L

for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let R be auxiliary(i) Relation of L; :: thesis: for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let C be strict_chain of R; :: thesis: for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let x, y be Element of L; :: thesis: ( x in C & y in C & x < y implies [x,y] in R )

assume that

A1: x in C and

A2: y in C and

A3: x < y ; :: thesis: [x,y] in R

( [x,y] in R or [y,x] in R ) by A1, A2, A3, Def3;

then ( [x,y] in R or y <= x ) by WAYBEL_4:def 3;

hence [x,y] in R by A3, ORDERS_2:6; :: thesis: verum

for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let R be auxiliary(i) Relation of L; :: thesis: for C being strict_chain of R

for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let C be strict_chain of R; :: thesis: for x, y being Element of L st x in C & y in C & x < y holds

[x,y] in R

let x, y be Element of L; :: thesis: ( x in C & y in C & x < y implies [x,y] in R )

assume that

A1: x in C and

A2: y in C and

A3: x < y ; :: thesis: [x,y] in R

( [x,y] in R or [y,x] in R ) by A1, A2, A3, Def3;

then ( [x,y] in R or y <= x ) by WAYBEL_4:def 3;

hence [x,y] in R by A3, ORDERS_2:6; :: thesis: verum