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: ex_sup_of SetBelow R,C,z,L by A1, A3;
A9: 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 A10: b in SetBelow R,C,z ; :: thesis: b <= x
then A11: not x < b by A7;

per cases ( x <> b or x = b ) ;

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

then A12: not x <= b by A11, ORDERS_2:def 10;
b in C by A10, Th18;
then ( [x,b] in R or x = b or [b,x] in R ) by A2, Def3;
hence b <= x by A12, WAYBEL_4:def 4; :: thesis: verum

end;

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

hence b <= x ; :: thesis: verum

end;

end;

end;

for a being Element of L st SetBelow R,C,z is_<=_than a holds
x <= a

proof

let a be Element of L; :: thesis: ( SetBelow R,C,z is_<=_than a implies x <= a )
assume A13: SetBelow R,C,z is_<=_than a ; :: thesis: x <= a
x in SetBelow R,C,z by A2, A4, Th18;
hence x <= a by A13, LATTICE3:def 9; :: thesis: verum

end;

hence ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) by A5, A6, A8, A9, 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, Th18; :: thesis: ( [x,y] in R & [y,z] in R & x <> y )
hence [x,y] in R by A2, A15, Th5; :: thesis: ( [y,z] in R & x <> y )
thus [y,z] in R by A14, Th18; :: thesis: x <> y
thus x <> y by A15; :: thesis: verum

end;

end;