let L be non empty reflexive antisymmetric RelStr ; :: thesis:
let R be auxiliary(i) Relation of L; :: thesis:
let C be strict_chain of R; :: thesis:
assume A1: for c being Element of L st c in C holds
( ex_sup_of SetBelow (R,C,c),L & c = sup (SetBelow (R,C,c)) ) ; :: thesis:
let x, z be Element of L; :: according to WAYBEL35:def 6 :: thesis:
assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z ; :: thesis:
A6: z = sup (SetBelow (R,C,z)) by A1, A3;

per cases ;

suppose A7: for y being Element of L holds
( not y in SetBelow (R,C,z) or not x < y ) ; :: thesis:

reconsider x = x as Element of L ;
A8: SetBelow (R,C,z) is_<=_than x

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume A9: b in SetBelow (R,C,z) ; :: thesis:
then A10: not x < b by A7;

per cases ;

suppose A11: x <> b ; :: thesis:

b in C by A9, Th15;
then A12: ( [x,b] in R or x = b or [b,x] in R ) by A2, Def3;
not x <= b by A11, A10, ORDERS_2:def 6;
hence b <= x by A12, WAYBEL_4:def 3; :: thesis:

end;

suppose x = b ; :: thesis:

hence b <= x ; :: thesis:

end;

end;

end;

A13: for a being Element of L st SetBelow (R,C,z) is_<=_than a holds
x <= a by A2, A4, Th15;
ex_sup_of SetBelow (R,C,z),L by A1, A3;
hence ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) by A13, A5, A6, A8, YELLOW_0:def 9; :: thesis:

end;

suppose ex y being Element of L st
( y in SetBelow (R,C,z) & x < y ) ; :: thesis:

then consider y being Element of L such that
A14: y in SetBelow (R,C,z) and
A15: x < y ;
take y ; :: thesis:
thus y in C by A14, Th15; :: thesis:
hence [x,y] in R by A2, A15, Th2; :: thesis:
thus [y,z] in R by A14, Th15; :: thesis:
thus x <> y by A15; :: thesis:

end;

end;