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: R satisfies_SIC_on C
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 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: verum

end;

suppose x = b ; :: thesis: b <= x

hence b <= x ; :: 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 A13, A5, A6, A8, YELLOW_0:def 9; :: 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 A14, Th15; :: 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 A14, Th15; :: thesis: x <> y
thus x <> y by A15; :: thesis: verum

end;

end;