let L be lower-bounded with_suprema Poset; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being strict_chain of R st C is maximal & R is satisfying_SI holds
R satisfies_SIC_on C
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being strict_chain of R st C is maximal & R is satisfying_SI holds
R satisfies_SIC_on C
let C be strict_chain of R; :: thesis: ( C is maximal & R is satisfying_SI implies R satisfies_SIC_on C )
assume that
A1: C is maximal and
A2: R is satisfying_SI ; :: 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
A3: x in C and
A4: z in C and
A5: [x,z] in R and
A6: x <> z ; :: thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
consider y being Element of L such that
A7: [x,y] in R and
A8: [y,z] in R and
A9: x <> y by A2, A5, A6, WAYBEL_4:def 20;
A10: y <= z by A8, WAYBEL_4:def 3;
assume A11: for y being Element of L holds
( not y in C or not [x,y] in R or not [y,z] in R or not x <> y ) ; :: thesis: contradiction
A12: x <= y by A7, WAYBEL_4:def 3;
A13: C \/ {y} is strict_chain of R

proof

let a, b be set ; :: according to WAYBEL35:def 3 :: thesis: ( a in C \/ {y} & b in C \/ {y} & not [a,b] in R & not a = b implies [b,a] in R )
assume that
A14: a in C \/ {y} and
A15: b in C \/ {y} ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

per cases ( ( a in C & b in C ) or ( a in C & b = y ) or ( a = y & b in C ) or ( a = y & b = y ) ) by A14, A15, Lm1;

suppose ( a in C & b in C ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by Def3; :: thesis: verum

end;

suppose that A16: a in C and
A17: b = y ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

now :: thesis: ( [a,b] in R or a = b or [b,a] in R )

reconsider a = a as Element of L by A16;
A18: a <= a ;

per cases ( x = a or a = z or ( not [x,a] in R & a <> x ) or ( not [a,z] in R & a <> z ) ) by A11, A16;

suppose x = a ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by A7, A17; :: thesis: verum

end;

suppose a = z ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A17; :: thesis: verum

end;

suppose ( not [x,a] in R & a <> x ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

then [a,x] in R by A3, A16, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A17, A18, WAYBEL_4:def 4; :: thesis: verum

end;

suppose ( not [a,z] in R & a <> z ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

then [z,a] in R by A4, A16, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A10, A17, A18, WAYBEL_4:def 4; :: thesis: verum

end;

end;

end;

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

suppose that A19: a = y and
A20: b in C ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

now :: thesis: ( [a,b] in R or a = b or [b,a] in R )

reconsider b = b as Element of L by A20;
A21: b <= b ;

per cases ( x = b or b = z or ( not [x,b] in R & b <> x ) or ( not [b,z] in R & b <> z ) ) by A11, A20;

suppose x = b ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by A7, A19; :: thesis: verum

end;

suppose b = z ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A19; :: thesis: verum

end;

suppose ( not [x,b] in R & b <> x ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

then [b,x] in R by A3, A20, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A19, A21, WAYBEL_4:def 4; :: thesis: verum

end;

suppose ( not [b,z] in R & b <> z ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

then [z,b] in R by A4, A20, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A10, A19, A21, WAYBEL_4:def 4; :: thesis: verum

end;

end;

end;

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

suppose ( a = y & b = y ) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

end;

end;

C c= C \/ {y} by XBOOLE_1:7;
then C \/ {y} = C by A13, A1;
then y in C by ZFMISC_1:39;
hence contradiction by A11, A7, A8, A9; :: thesis: verum