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:
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 ;
A10: y <= z by ;
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 ;
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 ;
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 ;
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 ; :: 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 ; :: 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 ;
hence ( [a,b] in R or a = b or [b,a] in R ) by ; :: 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 ;
hence ( [a,b] in R or a = b or [b,a] in R ) by ; :: 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 ;
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 ; :: 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 ; :: 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 ;
hence ( [a,b] in R or a = b or [b,a] in R ) by ; :: 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 ;
hence ( [a,b] in R or a = b or [b,a] in R ) by ; :: 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 ;
then y in C by ZFMISC_1:39;
hence contradiction by A11, A7, A8, A9; :: thesis: verum