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 )
assume A7: 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
consider y being Element of L such that
A8: [x,y] in R and
A9: [y,z] in R and
A10: x <> y by A2, A5, A6, WAYBEL_4:def 21;
A11: x <= y by A8, WAYBEL_4:def 4;
A12: y <= z by A9, WAYBEL_4:def 4;
A13: C c= C \/ {y} by XBOOLE_1:7;
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 A14: ( a in C \/ {y} & 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, 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 A15: a in C and
A16: b = y ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

now

reconsider a = a as Element of L by A15;
A17: 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 A7, A15;

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 A8, A16; :: 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 A9, A16; :: 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, A15, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A11, A16, A17, WAYBEL_4:def 5; :: 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, A15, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A16, A17, WAYBEL_4:def 5; :: thesis: verum

end;

end;

end;

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

end;

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

now

reconsider b = b as Element of L by A19;
A20: 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 A7, A19;

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 A8, A18; :: 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 A9, A18; :: 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, A19, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A11, A18, A20, WAYBEL_4:def 5; :: 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, A19, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A18, A20, WAYBEL_4:def 5; :: 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;

then C \/ {y} = C by A1, A13, Def4;
then y in C by ZFMISC_1:45;
hence contradiction by A7, A8, A9, A10; :: thesis: verum