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;

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 ) ) ;

end;

( 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 )

( 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

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;A8: SetBelow (R,C,z) is_<=_than x

proof

A13:
for a being Element of L st SetBelow (R,C,z) is_<=_than a holds
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;

end;assume A9: b in SetBelow (R,C,z) ; :: thesis: b <= x

then A10: not x < b by A7;

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

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 )

( 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;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