theorem Th2: :: WAYBEL35:2

for L being antisymmetric RelStr
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