let L be non empty reflexive antisymmetric RelStr ; :: thesis: for R being auxiliary(i) Relation of L
for C being strict_chain of R st ( 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)) ) ) holds
R satisfies_SIC_on C

let R be auxiliary(i) Relation of L; :: thesis: for C being strict_chain of R st ( 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)) ) ) holds
R satisfies_SIC_on C

let C be strict_chain of R; :: thesis: ( ( 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)) ) ) implies R satisfies_SIC_on C )

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: ( x in C & z in C & [x,z] in R & x <> z implies ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) )

assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )

A6: z = sup (SetBelow (R,C,z)) by A1, A3;
per cases ( for y being Element of L holds
( not y in SetBelow (R,C,z) or not x < y ) or ex y being Element of L st
( y in SetBelow (R,C,z) & x < y ) )
;
suppose A7: for y being Element of L holds
( not y in SetBelow (R,C,z) or not x < y ) ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )

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: ( not b in SetBelow (R,C,z) or b <= x )
assume A9: b in SetBelow (R,C,z) ; :: thesis: b <= x
then A10: not x < b by A7;
per cases ( x <> b or x = b ) ;
suppose A11: x <> b ; :: thesis: b <= x
b in C by ;
then A12: ( [x,b] in R or x = b or [b,x] in R ) by ;
not x <= b by ;
hence b <= x by ; :: thesis: verum
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 ; :: thesis: verum
end;
suppose ex y being Element of L st
( y in SetBelow (R,C,z) & x < y ) ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )

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