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

then C \/ {y} = C by A13, A1;

then y in C by ZFMISC_1:39;

hence contradiction by A11, A7, A8, A9; :: thesis: verum

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

C c= C \/ {y}
by XBOOLE_1:7;
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 )

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

end;

suppose that A16:
a in C
and

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

end;

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 )

hence
( [a,b] in R or a = b or [b,a] in R )
; :: thesis: verumreconsider a = a as Element of L by A16;

A18: a <= a ;

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

end;

suppose that A19:
a = y
and

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

end;

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 )

hence
( [a,b] in R or a = b or [b,a] in R )
; :: thesis: verumreconsider b = b as Element of L by A20;

A21: b <= b ;

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

end;

then C \/ {y} = C by A13, A1;

then y in C by ZFMISC_1:39;

hence contradiction by A11, A7, A8, A9; :: thesis: verum