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 & y in C ) and
A2: x < y ; :: thesis: [x,y] in R
( [x,y] in R or [y,x] in R ) by A1, A2, Def3;
then ( [x,y] in R or y <= x ) by WAYBEL_4:def 4;
hence [x,y] in R by A2, ORDERS_2:30; :: thesis: verum