:: WAYBEL35 semantic presentation begin Lm1: for x, y, X being set holds ( not y in {x} \/ X or y = x or y in X ) proof let x, y, X be set ; ::_thesis: ( not y in {x} \/ X or y = x or y in X ) assume y in {x} \/ X ; ::_thesis: ( y = x or y in X ) then ( y in {x} or y in X ) by XBOOLE_0:def_3; hence ( y = x or y in X ) by TARSKI:def_1; ::_thesis: verum end; begin registration let L be RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(i) proof take IntRel L ; ::_thesis: IntRel L is auxiliary(i) thus IntRel L is auxiliary(i) ; ::_thesis: verum end; end; registration let L be transitive RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st ( b1 is auxiliary(i) & b1 is auxiliary(ii) ) proof take IntRel L ; ::_thesis: ( IntRel L is auxiliary(i) & IntRel L is auxiliary(ii) ) thus ( IntRel L is auxiliary(i) & IntRel L is auxiliary(ii) ) ; ::_thesis: verum end; end; registration let L be antisymmetric with_suprema RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iii) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(iii) proof take IntRel L ; ::_thesis: IntRel L is auxiliary(iii) thus IntRel L is auxiliary(iii) ; ::_thesis: verum end; end; registration let L be non empty antisymmetric lower-bounded RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is auxiliary(iv) proof take IntRel L ; ::_thesis: IntRel L is auxiliary(iv) thus IntRel L is auxiliary(iv) ; ::_thesis: verum end; end; definition let L be non empty RelStr ; let R be Relation of L; attrR is extra-order means :Def1: :: WAYBEL35:def 1 ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ); end; :: deftheorem Def1 defines extra-order WAYBEL35:def_1_:_ for L being non empty RelStr for R being Relation of L holds ( R is extra-order iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ) ); registration let L be non empty RelStr ; cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is extra-order holds ( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) ) by Def1; cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) holds b1 is extra-order by Def1; end; registration let L be non empty RelStr ; cluster auxiliary(iii) extra-order -> auxiliary for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is extra-order & b1 is auxiliary(iii) holds b1 is auxiliary ; cluster auxiliary -> extra-order for Element of bool [: the carrier of L, the carrier of L:]; coherence for b1 being Relation of L st b1 is auxiliary holds b1 is extra-order ; end; registration let L be non empty transitive antisymmetric lower-bounded RelStr ; cluster Relation-like the carrier of L -defined the carrier of L -valued extra-order for Element of bool [: the carrier of L, the carrier of L:]; existence ex b1 being Relation of L st b1 is extra-order proof take IntRel L ; ::_thesis: IntRel L is extra-order thus IntRel L is extra-order ; ::_thesis: verum end; end; definition let L be lower-bounded with_suprema Poset; let R be auxiliary(ii) Relation of L; funcR -LowerMap -> Function of L,(InclPoset (LOWER L)) means :Def2: :: WAYBEL35:def 2 for x being Element of L holds it . x = R -below x; existence ex b1 being Function of L,(InclPoset (LOWER L)) st for x being Element of L holds b1 . x = R -below x proof deffunc H1( Element of L) -> Element of bool the carrier of L = R -below \$1; A1: for x being Element of L holds H1(x) is Element of (InclPoset (LOWER L)) proof let x be Element of L; ::_thesis: H1(x) is Element of (InclPoset (LOWER L)) reconsider I = H1(x) as lower Subset of L ; LOWER L = { X where X is Subset of L : X is lower } by LATTICE7:def_7; then I in LOWER L ; hence H1(x) is Element of (InclPoset (LOWER L)) by YELLOW_1:1; ::_thesis: verum end; consider f being Function of L,(InclPoset (LOWER L)) such that A2: for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_9(A1); take f ; ::_thesis: for x being Element of L holds f . x = R -below x let x be Element of L; ::_thesis: f . x = R -below x thus f . x = R -below x by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of L,(InclPoset (LOWER L)) st ( for x being Element of L holds b1 . x = R -below x ) & ( for x being Element of L holds b2 . x = R -below x ) holds b1 = b2 proof let M1, M2 be Function of L,(InclPoset (LOWER L)); ::_thesis: ( ( for x being Element of L holds M1 . x = R -below x ) & ( for x being Element of L holds M2 . x = R -below x ) implies M1 = M2 ) assume A3: for x being Element of L holds M1 . x = R -below x ; ::_thesis: ( ex x being Element of L st not M2 . x = R -below x or M1 = M2 ) assume A4: for x being Element of L holds M2 . x = R -below x ; ::_thesis: M1 = M2 for x being set st x in the carrier of L holds M1 . x = M2 . x proof let x be set ; ::_thesis: ( x in the carrier of L implies M1 . x = M2 . x ) assume x in the carrier of L ; ::_thesis: M1 . x = M2 . x then reconsider x9 = x as Element of L ; thus M1 . x = R -below x9 by A3 .= M2 . x by A4 ; ::_thesis: verum end; hence M1 = M2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def2 defines -LowerMap WAYBEL35:def_2_:_ for L being lower-bounded with_suprema Poset for R being auxiliary(ii) Relation of L for b3 being Function of L,(InclPoset (LOWER L)) holds ( b3 = R -LowerMap iff for x being Element of L holds b3 . x = R -below x ); registration let L be lower-bounded with_suprema Poset; let R be auxiliary(ii) Relation of L; clusterR -LowerMap -> monotone ; coherence R -LowerMap is monotone proof let x, y be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (R -LowerMap) . x <= (R -LowerMap) . y ) set s = R -LowerMap ; A1: (R -LowerMap) . y = R -below y by Def2; assume x <= y ; ::_thesis: (R -LowerMap) . x <= (R -LowerMap) . y then A2: R -below x c= R -below y by WAYBEL_4:17; (R -LowerMap) . x = R -below x by Def2; hence (R -LowerMap) . x <= (R -LowerMap) . y by A2, A1, YELLOW_1:3; ::_thesis: verum end; end; definition let L be 1-sorted ; let R be Relation of the carrier of L; mode strict_chain of R -> Subset of L means :Def3: :: WAYBEL35:def 3 for x, y being set st x in it & y in it & not [x,y] in R & not x = y holds [y,x] in R; existence ex b1 being Subset of L st for x, y being set st x in b1 & y in b1 & not [x,y] in R & not x = y holds [y,x] in R proof take {} L ; ::_thesis: for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds [y,x] in R thus for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds [y,x] in R ; ::_thesis: verum end; end; :: deftheorem Def3 defines strict_chain WAYBEL35:def_3_:_ for L being 1-sorted for R being Relation of the carrier of L for b3 being Subset of L holds ( b3 is strict_chain of R iff for x, y being set st x in b3 & y in b3 & not [x,y] in R & not x = y holds [y,x] in R ); theorem Th1: :: WAYBEL35:1 for L being 1-sorted for C being trivial Subset of L for R being Relation of the carrier of L holds C is strict_chain of R proof let L be 1-sorted ; ::_thesis: for C being trivial Subset of L for R being Relation of the carrier of L holds C is strict_chain of R let C be trivial Subset of L; ::_thesis: for R being Relation of the carrier of L holds C is strict_chain of R let R be Relation of the carrier of L; ::_thesis: C is strict_chain of R let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R ) thus ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R ) by SUBSET_1:def_7; ::_thesis: verum end; registration let L be non empty 1-sorted ; let R be Relation of the carrier of L; cluster1 -element for strict_chain of R; existence ex b1 being strict_chain of R st b1 is 1 -element proof set C = the 1 -element Subset of L; reconsider C = the 1 -element Subset of L as strict_chain of R by Th1; take C ; ::_thesis: C is 1 -element thus C is 1 -element ; ::_thesis: verum end; end; theorem Th2: :: WAYBEL35:2 for L being antisymmetric RelStr for R being auxiliary(i) Relation of L for C being strict_chain of R for x, y being Element of L st x in C & y in C & x < y holds [x,y] in R proof let L be antisymmetric RelStr ; ::_thesis: for R being auxiliary(i) Relation of L for C being strict_chain of R for x, y being Element of L st x in C & y in C & x < y holds [x,y] in R let R be auxiliary(i) Relation of L; ::_thesis: for C being strict_chain of R for x, y being Element of L st x in C & y in C & x < y holds [x,y] in R let C be strict_chain of R; ::_thesis: for x, y being Element of L st x in C & y in C & x < y holds [x,y] in R let x, y be Element of L; ::_thesis: ( x in C & y in C & x < y implies [x,y] in R ) assume that A1: x in C and A2: y in C and A3: x < y ; ::_thesis: [x,y] in R ( [x,y] in R or [y,x] in R ) by A1, A2, A3, Def3; then ( [x,y] in R or y <= x ) by WAYBEL_4:def_3; hence [x,y] in R by A3, ORDERS_2:6; ::_thesis: verum end; theorem :: WAYBEL35:3 for L being antisymmetric RelStr for R being auxiliary(i) Relation of L for x, y being Element of L st [x,y] in R & [y,x] in R holds x = y proof let L be antisymmetric RelStr ; ::_thesis: for R being auxiliary(i) Relation of L for x, y being Element of L st [x,y] in R & [y,x] in R holds x = y let R be auxiliary(i) Relation of L; ::_thesis: for x, y being Element of L st [x,y] in R & [y,x] in R holds x = y let x, y be Element of L; ::_thesis: ( [x,y] in R & [y,x] in R implies x = y ) assume that A1: [x,y] in R and A2: [y,x] in R ; ::_thesis: x = y A3: y <= x by A2, WAYBEL_4:def_3; x <= y by A1, WAYBEL_4:def_3; hence x = y by A3, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL35:4 for L being non empty antisymmetric lower-bounded RelStr for x being Element of L for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R let x be Element of L; ::_thesis: for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R let R be auxiliary(iv) Relation of L; ::_thesis: {(Bottom L),x} is strict_chain of R let a, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in {(Bottom L),x} & y in {(Bottom L),x} & not [a,y] in R & not a = y implies [y,a] in R ) assume that A1: a in {(Bottom L),x} and A2: y in {(Bottom L),x} ; ::_thesis: ( [a,y] in R or a = y or [y,a] in R ) A3: ( y = Bottom L or y = x ) by A2, TARSKI:def_2; ( a = Bottom L or a = x ) by A1, TARSKI:def_2; hence ( [a,y] in R or a = y or [y,a] in R ) by A3, WAYBEL_4:def_6; ::_thesis: verum end; theorem Th5: :: WAYBEL35:5 for L being non empty antisymmetric lower-bounded RelStr for R being auxiliary(iv) Relation of L for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for R being auxiliary(iv) Relation of L for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R let R be auxiliary(iv) Relation of L; ::_thesis: for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R let C be strict_chain of R; ::_thesis: C \/ {(Bottom L)} is strict_chain of R set A = C \/ {(Bottom L)}; let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in C \/ {(Bottom L)} & y in C \/ {(Bottom L)} & not [x,y] in R & not x = y implies [y,x] in R ) assume that A1: x in C \/ {(Bottom L)} and A2: y in C \/ {(Bottom L)} ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) reconsider x = x, y = y as Element of L by A1, A2; percases ( ( x in C & y in C ) or ( x in C & y = Bottom L ) or ( x = Bottom L & y in C ) or ( x = Bottom L & y = Bottom L ) ) by A1, A2, Lm1; suppose ( x in C & y in C ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) hence ( [x,y] in R or x = y or [y,x] in R ) by Def3; ::_thesis: verum end; suppose ( x in C & y = Bottom L ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def_6; ::_thesis: verum end; suppose ( x = Bottom L & y in C ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def_6; ::_thesis: verum end; suppose ( x = Bottom L & y = Bottom L ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) hence ( [x,y] in R or x = y or [y,x] in R ) ; ::_thesis: verum end; end; end; definition let L be 1-sorted ; let R be Relation of the carrier of L; let C be strict_chain of R; attrC is maximal means :Def4: :: WAYBEL35:def 4 for D being strict_chain of R st C c= D holds C = D; end; :: deftheorem Def4 defines maximal WAYBEL35:def_4_:_ for L being 1-sorted for R being Relation of the carrier of L for C being strict_chain of R holds ( C is maximal iff for D being strict_chain of R st C c= D holds C = D ); definition let L be 1-sorted ; let R be Relation of the carrier of L; let C be set ; defpred S1[ set ] means ( \$1 is strict_chain of R & C c= \$1 ); func Strict_Chains (R,C) -> set means :Def5: :: WAYBEL35:def 5 for x being set holds ( x in it iff ( x is strict_chain of R & C c= x ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x is strict_chain of R & C c= x ) ) proof consider X being set such that A1: for x being set holds ( x in X iff ( x in bool the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ( x is strict_chain of R & C c= x ) ) thus for x being set holds ( x in X iff ( x is strict_chain of R & C c= x ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x is strict_chain of R & C c= x ) ) ) & ( for x being set holds ( x in b2 iff ( x is strict_chain of R & C c= x ) ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def5 defines Strict_Chains WAYBEL35:def_5_:_ for L being 1-sorted for R being Relation of the carrier of L for C being set for b4 being set holds ( b4 = Strict_Chains (R,C) iff for x being set holds ( x in b4 iff ( x is strict_chain of R & C c= x ) ) ); registration let L be 1-sorted ; let R be Relation of the carrier of L; let C be strict_chain of R; cluster Strict_Chains (R,C) -> non empty ; coherence not Strict_Chains (R,C) is empty by Def5; end; notation let R be Relation; let X be set ; synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R; end; theorem :: WAYBEL35:6 for L being 1-sorted for R being Relation of the carrier of L for C being strict_chain of R holds ( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) ) proof let L be 1-sorted ; ::_thesis: for R being Relation of the carrier of L for C being strict_chain of R holds ( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) ) let R be Relation of the carrier of L; ::_thesis: for C being strict_chain of R holds ( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) ) let C be strict_chain of R; ::_thesis: ( Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) & ex D being set st ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) ) set X = Strict_Chains (R,C); A1: field (RelIncl (Strict_Chains (R,C))) = Strict_Chains (R,C) by WELLORD2:def_1; thus A2: Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) ::_thesis: ex D being set st ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) proof let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( not Y c= Strict_Chains (R,C) or not (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order or ex b1 being set st ( b1 in Strict_Chains (R,C) & ( for b2 being set holds ( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) ) assume that A3: Y c= Strict_Chains (R,C) and A4: (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order ; ::_thesis: ex b1 being set st ( b1 in Strict_Chains (R,C) & ( for b2 being set holds ( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) percases ( Y is empty or not Y is empty ) ; supposeA5: Y is empty ; ::_thesis: ex b1 being set st ( b1 in Strict_Chains (R,C) & ( for b2 being set holds ( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) take C ; ::_thesis: ( C in Strict_Chains (R,C) & ( for b1 being set holds ( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) ) thus ( C in Strict_Chains (R,C) & ( for b1 being set holds ( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) ) by A5, Def5; ::_thesis: verum end; supposeA6: not Y is empty ; ::_thesis: ex b1 being set st ( b1 in Strict_Chains (R,C) & ( for b2 being set holds ( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) take Z = union Y; ::_thesis: ( Z in Strict_Chains (R,C) & ( for b1 being set holds ( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) ) ) ) Z c= the carrier of L proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in the carrier of L ) assume z in Z ; ::_thesis: z in the carrier of L then consider A being set such that A7: z in A and A8: A in Y by TARSKI:def_4; A is strict_chain of R by A3, A8, Def5; hence z in the carrier of L by A7; ::_thesis: verum end; then reconsider S = Z as Subset of L ; A9: S is strict_chain of R proof (RelIncl (Strict_Chains (R,C))) |_2 Y is connected by A4, ORDERS_1:def_5; then A10: (RelIncl (Strict_Chains (R,C))) |_2 Y is_connected_in field ((RelIncl (Strict_Chains (R,C))) |_2 Y) by RELAT_2:def_14; A11: (RelIncl (Strict_Chains (R,C))) |_2 Y = RelIncl Y by A3, WELLORD2:7; let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in S & y in S & not [x,y] in R & not x = y implies [y,x] in R ) A12: field (RelIncl Y) = Y by WELLORD2:def_1; assume x in S ; ::_thesis: ( not y in S or [x,y] in R or x = y or [y,x] in R ) then consider A being set such that A13: x in A and A14: A in Y by TARSKI:def_4; A15: A is strict_chain of R by A3, A14, Def5; assume y in S ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) then consider B being set such that A16: y in B and A17: B in Y by TARSKI:def_4; A18: B is strict_chain of R by A3, A17, Def5; percases ( A <> B or A = B ) ; suppose A <> B ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) then ( [A,B] in RelIncl Y or [B,A] in RelIncl Y ) by A14, A17, A10, A11, A12, RELAT_2:def_6; then ( A c= B or B c= A ) by A14, A17, WELLORD2:def_1; hence ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, A18, Def3; ::_thesis: verum end; suppose A = B ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R ) hence ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, Def3; ::_thesis: verum end; end; end; C c= Z proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in Z ) assume A19: c in C ; ::_thesis: c in Z consider y being set such that A20: y in Y by A6, XBOOLE_0:def_1; C c= y by A3, A20, Def5; hence c in Z by A19, A20, TARSKI:def_4; ::_thesis: verum end; hence A21: Z in Strict_Chains (R,C) by A9, Def5; ::_thesis: for b1 being set holds ( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) ) let y be set ; ::_thesis: ( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) ) assume A22: y in Y ; ::_thesis: [y,Z] in RelIncl (Strict_Chains (R,C)) then y c= Z by ZFMISC_1:74; hence [y,Z] in RelIncl (Strict_Chains (R,C)) by A3, A21, A22, WELLORD2:def_1; ::_thesis: verum end; end; end; A23: RelIncl (Strict_Chains (R,C)) is_transitive_in Strict_Chains (R,C) by WELLORD2:20; A24: RelIncl (Strict_Chains (R,C)) is_antisymmetric_in Strict_Chains (R,C) by WELLORD2:21; RelIncl (Strict_Chains (R,C)) is_reflexive_in Strict_Chains (R,C) by WELLORD2:19; then RelIncl (Strict_Chains (R,C)) partially_orders Strict_Chains (R,C) by A23, A24, ORDERS_1:def_7; then consider D being set such that A25: D is_maximal_in RelIncl (Strict_Chains (R,C)) by A1, A2, ORDERS_1:63; take D ; ::_thesis: ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D ) thus D is_maximal_in RelIncl (Strict_Chains (R,C)) by A25; ::_thesis: C c= D D in field (RelIncl (Strict_Chains (R,C))) by A25, ORDERS_1:def_11; hence C c= D by A1, Def5; ::_thesis: verum end; theorem Th7: :: WAYBEL35:7 for L being non empty transitive RelStr for C being non empty Subset of L for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) proof let L be non empty transitive RelStr ; ::_thesis: for C being non empty Subset of L for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) let C be non empty Subset of L; ::_thesis: for X being Subset of C st ex_sup_of X,L & "\/" (X,L) in C holds ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) let X be Subset of C; ::_thesis: ( ex_sup_of X,L & "\/" (X,L) in C implies ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) ) assume that A1: ex_sup_of X,L and A2: "\/" (X,L) in C ; ::_thesis: ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) the carrier of (subrelstr C) = C by YELLOW_0:def_15; hence ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) by A1, A2, YELLOW_0:64; ::_thesis: verum end; Lm2: for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) proof let L be non empty Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) let C be non empty strict_chain of R; ::_thesis: for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) let X be Subset of C; ::_thesis: ( ex_sup_of X,L & C is maximal & not "\/" (X,L) in C implies ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) ) assume that A1: ex_sup_of X,L and A2: C is maximal ; ::_thesis: ( "\/" (X,L) in C or ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) ) set s = "\/" (X,L); A3: C c= C \/ {("\/" (X,L))} by XBOOLE_1:7; assume A4: not "\/" (X,L) in C ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) then not C \/ {("\/" (X,L))} c= C by ZFMISC_1:39; then A5: C \/ {("\/" (X,L))} is not strict_chain of R by A3, A2, Def4; ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) proof A6: for a being Element of L st a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R holds ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) proof let a be Element of L; ::_thesis: ( a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R implies ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) ) assume that A7: a in C and A8: not [a,("\/" (X,L))] in R and A9: not [("\/" (X,L)),a] in R ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) take a ; ::_thesis: ( a in C & "\/" (X,L) < a & not [("\/" (X,L)),a] in R ) thus a in C by A7; ::_thesis: ( "\/" (X,L) < a & not [("\/" (X,L)),a] in R ) a is_>=_than X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= a ) assume A10: x in X ; ::_thesis: x <= a percases ( [a,x] in R or [x,a] in R or a = x ) by A7, A10, Def3; supposeA11: [a,x] in R ; ::_thesis: x <= a A12: a <= a ; x <= "\/" (X,L) by A1, A10, YELLOW_4:1; hence x <= a by A12, A8, A11, WAYBEL_4:def_4; ::_thesis: verum end; suppose ( [x,a] in R or a = x ) ; ::_thesis: x <= a hence x <= a by WAYBEL_4:def_3; ::_thesis: verum end; end; end; then "\/" (X,L) <= a by A1, YELLOW_0:def_9; hence "\/" (X,L) < a by A4, A7, ORDERS_2:def_6; ::_thesis: not [("\/" (X,L)),a] in R thus not [("\/" (X,L)),a] in R by A9; ::_thesis: verum end; consider a, b being set such that A13: a in C \/ {("\/" (X,L))} and A14: b in C \/ {("\/" (X,L))} and A15: not [a,b] in R and A16: a <> b and A17: not [b,a] in R by A5, Def3; reconsider a = a, b = b as Element of L by A13, A14; percases ( ( a in C & b in C ) or ( a in C & b = "\/" (X,L) ) or ( a = "\/" (X,L) & b in C ) or ( a = "\/" (X,L) & b = "\/" (X,L) ) ) by A13, A14, Lm1; suppose ( a in C & b in C ) ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) hence ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A16, A17, Def3; ::_thesis: verum end; suppose ( a in C & b = "\/" (X,L) ) ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) hence ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; ::_thesis: verum end; suppose ( a = "\/" (X,L) & b in C ) ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) hence ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; ::_thesis: verum end; suppose ( a = "\/" (X,L) & b = "\/" (X,L) ) ; ::_thesis: ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) hence ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A16; ::_thesis: verum end; end; end; then consider cs being Element of L such that A18: cs in C and A19: "\/" (X,L) < cs and A20: not [("\/" (X,L)),cs] in R ; take cs ; ::_thesis: ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A18, A19, A20; ::_thesis: ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) reconsider cs1 = cs as Element of (subrelstr C) by A18, YELLOW_0:def_15; take cs1 ; ::_thesis: ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) thus cs = cs1 ; ::_thesis: ( X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) A21: "\/" (X,L) <= cs by A19, ORDERS_2:def_6; thus X is_<=_than cs1 ::_thesis: for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a proof let b be Element of (subrelstr C); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= cs1 ) reconsider b0 = b as Element of L by YELLOW_0:58; assume b in X ; ::_thesis: b <= cs1 then b0 <= "\/" (X,L) by A1, YELLOW_4:1; then b0 <= cs by A21, ORDERS_2:3; hence b <= cs1 by YELLOW_0:60; ::_thesis: verum end; let a be Element of (subrelstr C); ::_thesis: ( X is_<=_than a implies cs1 <= a ) reconsider a0 = a as Element of L by YELLOW_0:58; A22: the carrier of (subrelstr C) = C by YELLOW_0:def_15; assume X is_<=_than a ; ::_thesis: cs1 <= a then X is_<=_than a0 by A22, YELLOW_0:62; then A23: "\/" (X,L) <= a0 by A1, YELLOW_0:def_9; A24: cs <= cs ; ( [cs1,a] in R or a = cs1 or [a,cs1] in R ) by A22, Def3; then cs <= a0 by A20, A23, A24, WAYBEL_4:def_3, WAYBEL_4:def_4; hence cs1 <= a by YELLOW_0:60; ::_thesis: verum end; theorem Th8: :: WAYBEL35:8 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal holds ex_sup_of X, subrelstr C proof let L be non empty Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal holds ex_sup_of X, subrelstr C let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R for X being Subset of C st ex_sup_of X,L & C is maximal holds ex_sup_of X, subrelstr C let C be non empty strict_chain of R; ::_thesis: for X being Subset of C st ex_sup_of X,L & C is maximal holds ex_sup_of X, subrelstr C let X be Subset of C; ::_thesis: ( ex_sup_of X,L & C is maximal implies ex_sup_of X, subrelstr C ) assume that A1: ex_sup_of X,L and A2: C is maximal ; ::_thesis: ex_sup_of X, subrelstr C set s = "\/" (X,L); percases ( "\/" (X,L) in C or not "\/" (X,L) in C ) ; suppose "\/" (X,L) in C ; ::_thesis: ex_sup_of X, subrelstr C hence ex_sup_of X, subrelstr C by A1, Th7; ::_thesis: verum end; suppose not "\/" (X,L) in C ; ::_thesis: ex_sup_of X, subrelstr C then ex cs being Element of L st ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) ) by A1, A2, Lm2; hence ex_sup_of X, subrelstr C by YELLOW_0:15; ::_thesis: verum end; end; end; theorem :: WAYBEL35:9 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) proof let L be non empty Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) let C be non empty strict_chain of R; ::_thesis: for X being Subset of C st ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal holds ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) let X be Subset of C; ::_thesis: ( ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal implies ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) ) set s = "\/" (X,L); set x = "\/" (X,(subrelstr C)); set U = uparrow ("\/" (X,L)); assume that A1: ex_inf_of (uparrow ("\/" (X,L))) /\ C,L and A2: ex_sup_of X,L and A3: C is maximal ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) A4: "\/" (X,L) <= "\/" (X,L) ; reconsider x1 = "\/" (X,(subrelstr C)) as Element of L by YELLOW_0:58; A5: the carrier of (subrelstr C) = C by YELLOW_0:def_15; percases ( "\/" (X,L) in C or not "\/" (X,L) in C ) ; supposeA6: "\/" (X,L) in C ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) then A7: "\/" (X,L) = "\/" (X,(subrelstr C)) by A2, A5, YELLOW_0:64; A8: (uparrow ("\/" (X,L))) /\ C is_>=_than x1 proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow ("\/" (X,L))) /\ C or x1 <= b ) assume b in (uparrow ("\/" (X,L))) /\ C ; ::_thesis: x1 <= b then b in uparrow ("\/" (X,L)) by XBOOLE_0:def_4; hence x1 <= b by A7, WAYBEL_0:18; ::_thesis: verum end; for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds a <= x1 proof "\/" (X,L) in uparrow ("\/" (X,L)) by A4, WAYBEL_0:18; then A9: x1 in (uparrow ("\/" (X,L))) /\ C by A6, A7, XBOOLE_0:def_4; let a be Element of L; ::_thesis: ( (uparrow ("\/" (X,L))) /\ C is_>=_than a implies a <= x1 ) assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; ::_thesis: a <= x1 hence a <= x1 by A9, LATTICE3:def_8; ::_thesis: verum end; hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A1, A6, A8, YELLOW_0:def_10; ::_thesis: verum end; suppose not "\/" (X,L) in C ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) then consider cs being Element of L such that A10: cs in C and A11: "\/" (X,L) < cs and A12: not [("\/" (X,L)),cs] in R and A13: ex cs1 being Element of (subrelstr C) st ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds cs1 <= a ) ) by A2, A3, Lm2; A14: "\/" (X,L) <= cs by A11, ORDERS_2:def_6; A15: for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds a <= cs proof cs in uparrow ("\/" (X,L)) by A14, WAYBEL_0:18; then A16: cs in (uparrow ("\/" (X,L))) /\ C by A10, XBOOLE_0:def_4; let a be Element of L; ::_thesis: ( (uparrow ("\/" (X,L))) /\ C is_>=_than a implies a <= cs ) assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; ::_thesis: a <= cs hence a <= cs by A16, LATTICE3:def_8; ::_thesis: verum end; A17: cs <= cs ; A18: (uparrow ("\/" (X,L))) /\ C is_>=_than cs proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow ("\/" (X,L))) /\ C or cs <= b ) assume A19: b in (uparrow ("\/" (X,L))) /\ C ; ::_thesis: cs <= b then b in uparrow ("\/" (X,L)) by XBOOLE_0:def_4; then A20: "\/" (X,L) <= b by WAYBEL_0:18; b in C by A19, XBOOLE_0:def_4; then ( [b,cs] in R or b = cs or [cs,b] in R ) by A10, Def3; hence cs <= b by A12, A17, A20, WAYBEL_4:def_3, WAYBEL_4:def_4; ::_thesis: verum end; ex_sup_of X, subrelstr C by A2, A3, Th8; then cs = "\/" (X,(subrelstr C)) by A13, YELLOW_0:def_9; hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A15, A1, A11, A18, YELLOW_0:def_10; ::_thesis: verum end; end; end; theorem :: WAYBEL35:10 for L being non empty complete Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R st C is maximal holds subrelstr C is complete proof let L be non empty complete Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being non empty strict_chain of R st C is maximal holds subrelstr C is complete let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R st C is maximal holds subrelstr C is complete let C be non empty strict_chain of R; ::_thesis: ( C is maximal implies subrelstr C is complete ) assume A1: C is maximal ; ::_thesis: subrelstr C is complete for X being Subset of (subrelstr C) holds ex_sup_of X, subrelstr C proof let X be Subset of (subrelstr C); ::_thesis: ex_sup_of X, subrelstr C X is Subset of C by YELLOW_0:def_15; hence ex_sup_of X, subrelstr C by A1, Th8, YELLOW_0:17; ::_thesis: verum end; hence subrelstr C is complete by YELLOW_0:53; ::_thesis: verum end; theorem :: WAYBEL35:11 for L being non empty antisymmetric lower-bounded RelStr for R being auxiliary(iv) Relation of L for C being strict_chain of R st C is maximal holds Bottom L in C proof let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for R being auxiliary(iv) Relation of L for C being strict_chain of R st C is maximal holds Bottom L in C let R be auxiliary(iv) Relation of L; ::_thesis: for C being strict_chain of R st C is maximal holds Bottom L in C let C be strict_chain of R; ::_thesis: ( C is maximal implies Bottom L in C ) assume A1: for D being strict_chain of R st C c= D holds C = D ; :: according to WAYBEL35:def_4 ::_thesis: Bottom L in C C \/ {(Bottom L)} is strict_chain of R by Th5; then A2: C \/ {(Bottom L)} = C by A1, XBOOLE_1:7; assume not Bottom L in C ; ::_thesis: contradiction then not Bottom L in {(Bottom L)} by A2, XBOOLE_0:def_3; hence contradiction by TARSKI:def_1; ::_thesis: verum end; theorem :: WAYBEL35:12 for L being non empty upper-bounded Poset for R being auxiliary(ii) Relation of L for C being strict_chain of R for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds ( [(Top L),(Top L)] in R & m = Top L ) proof let L be non empty upper-bounded Poset; ::_thesis: for R being auxiliary(ii) Relation of L for C being strict_chain of R for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds ( [(Top L),(Top L)] in R & m = Top L ) let R be auxiliary(ii) Relation of L; ::_thesis: for C being strict_chain of R for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds ( [(Top L),(Top L)] in R & m = Top L ) let C be strict_chain of R; ::_thesis: for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds ( [(Top L),(Top L)] in R & m = Top L ) let m be Element of L; ::_thesis: ( C is maximal & m is_maximum_of C & [m,(Top L)] in R implies ( [(Top L),(Top L)] in R & m = Top L ) ) assume that A1: C is maximal and A2: m is_maximum_of C and A3: [m,(Top L)] in R ; ::_thesis: ( [(Top L),(Top L)] in R & m = Top L ) A4: C c= C \/ {(Top L)} by XBOOLE_1:7; now__::_thesis:_not_m_<>_Top_L A5: m <= Top L by YELLOW_0:45; assume A6: m <> Top L ; ::_thesis: contradiction A7: {(Top L)} c= C \/ {(Top L)} by XBOOLE_1:7; A8: ex_sup_of C,L by A2, WAYBEL_1:def_7; A9: sup C = m by A2, WAYBEL_1:def_7; C \/ {(Top L)} is strict_chain of R proof let a, b be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in C \/ {(Top L)} & b in C \/ {(Top L)} & not [a,b] in R & not a = b implies [b,a] in R ) assume that A10: a in C \/ {(Top L)} and A11: b in C \/ {(Top L)} ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) A12: Top L <= Top L ; percases ( ( a in C & b in C ) or ( a = Top L & b in C ) or ( a in C & b = Top L ) or ( a = Top L & b = Top L ) ) by A10, A11, 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; supposethat A13: a = Top L and A14: b in C ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) reconsider b = b as Element of L by A14; b <= sup C by A8, A14, YELLOW_4:1; hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A13, WAYBEL_4:def_4; ::_thesis: verum end; supposethat A15: a in C and A16: b = Top L ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) reconsider a = a as Element of L by A15; a <= sup C by A8, A15, YELLOW_4:1; hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A16, WAYBEL_4:def_4; ::_thesis: verum end; suppose ( a = Top L & b = Top L ) ; ::_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 A17: C \/ {(Top L)} = C by A1, A4, Def4; Top L in {(Top L)} by TARSKI:def_1; then Top L <= sup C by A7, A8, A17, YELLOW_4:1; hence contradiction by A6, A5, A9, ORDERS_2:2; ::_thesis: verum end; hence ( [(Top L),(Top L)] in R & m = Top L ) by A3; ::_thesis: verum end; definition let L be RelStr ; let C be set ; let R be Relation of the carrier of L; predR satisfies_SIC_on C means :Def6: :: WAYBEL35:def 6 for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ); end; :: deftheorem Def6 defines satisfies_SIC_on WAYBEL35:def_6_:_ for L being RelStr for C being set for R being Relation of the carrier of L holds ( R satisfies_SIC_on C iff for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ) ); definition let L be RelStr ; let R be Relation of the carrier of L; let C be strict_chain of R; attrC is satisfying_SIC means :Def7: :: WAYBEL35:def 7 R satisfies_SIC_on C; end; :: deftheorem Def7 defines satisfying_SIC WAYBEL35:def_7_:_ for L being RelStr for R being Relation of the carrier of L for C being strict_chain of R holds ( C is satisfying_SIC iff R satisfies_SIC_on C ); theorem Th13: :: WAYBEL35:13 for L being RelStr for C being set for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) proof let L be RelStr ; ::_thesis: for C being set for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) let C be set ; ::_thesis: for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) let R be auxiliary(i) Relation of L; ::_thesis: ( R satisfies_SIC_on C implies for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) ) assume A1: R satisfies_SIC_on C ; ::_thesis: for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x < y ) let x, z be Element of L; ::_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 ) consider y being Element of L such that A6: y in C and A7: [x,y] in R and A8: [y,z] in R and A9: x <> y by A2, A3, A4, A5, A1, Def6; take y ; ::_thesis: ( y in C & [x,y] in R & [y,z] in R & x < y ) thus ( y in C & [x,y] in R & [y,z] in R ) by A6, A7, A8; ::_thesis: x < y x <= y by A7, WAYBEL_4:def_3; hence x < y by A9, ORDERS_2:def_6; ::_thesis: verum end; registration let L be RelStr ; let R be Relation of the carrier of L; cluster trivial -> satisfying_SIC for strict_chain of R; coherence for b1 being strict_chain of R st b1 is trivial holds b1 is satisfying_SIC proof let C be strict_chain of R; ::_thesis: ( C is trivial implies C is satisfying_SIC ) assume A1: C is trivial ; ::_thesis: C is satisfying_SIC let x, z be Element of L; :: according to WAYBEL35:def_6,WAYBEL35:def_7 ::_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 [x,z] in R and A4: x <> z ; ::_thesis: ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ) thus ex y being Element of L st ( y in C & [x,y] in R & [y,z] in R & x <> y ) by A2, A3, A4, A1, SUBSET_1:def_7; ::_thesis: verum end; end; registration let L be non empty RelStr ; let R be Relation of the carrier of L; cluster1 -element for strict_chain of R; existence ex b1 being strict_chain of R st b1 is 1 -element proof set C = the 1 -element Subset of L; reconsider C = the 1 -element Subset of L as strict_chain of R by Th1; take C ; ::_thesis: C is 1 -element thus C is 1 -element ; ::_thesis: verum end; end; theorem :: WAYBEL35:14 for L being lower-bounded with_suprema Poset 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 proof 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 ) percases ( ( 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; supposethat 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 ; percases ( 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; supposethat 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 ; percases ( 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, Def4; then y in C by ZFMISC_1:39; hence contradiction by A11, A7, A8, A9; ::_thesis: verum end; definition let R be Relation; let C, y be set ; func SetBelow (R,C,y) -> set equals :: WAYBEL35:def 8 (R " {y}) /\ C; coherence (R " {y}) /\ C is set ; end; :: deftheorem defines SetBelow WAYBEL35:def_8_:_ for R being Relation for C, y being set holds SetBelow (R,C,y) = (R " {y}) /\ C; theorem Th15: :: WAYBEL35:15 for R being Relation for C, x, y being set holds ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) ) proof let R be Relation; ::_thesis: for C, x, y being set holds ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) ) let C, x, y be set ; ::_thesis: ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) ) hereby ::_thesis: ( [x,y] in R & x in C implies x in SetBelow (R,C,y) ) assume A1: x in SetBelow (R,C,y) ; ::_thesis: ( [x,y] in R & x in C ) then x in R " {y} by XBOOLE_0:def_4; then ex a being set st ( [x,a] in R & a in {y} ) by RELAT_1:def_14; hence [x,y] in R by TARSKI:def_1; ::_thesis: x in C thus x in C by A1, XBOOLE_0:def_4; ::_thesis: verum end; assume that A2: [x,y] in R and A3: x in C ; ::_thesis: x in SetBelow (R,C,y) y in {y} by TARSKI:def_1; then x in R " {y} by A2, RELAT_1:def_14; hence x in SetBelow (R,C,y) by A3, XBOOLE_0:def_4; ::_thesis: verum end; definition let L be 1-sorted ; let R be Relation of the carrier of L; let C, y be set ; :: original: SetBelow redefine func SetBelow (R,C,y) -> Subset of L; coherence SetBelow (R,C,y) is Subset of L proof (R " {y}) /\ C c= the carrier of L ; hence SetBelow (R,C,y) is Subset of L ; ::_thesis: verum end; end; theorem Th16: :: WAYBEL35:16 for L being RelStr for R being auxiliary(i) Relation of L for C being set for y being Element of L holds SetBelow (R,C,y) is_<=_than y proof let L be RelStr ; ::_thesis: for R being auxiliary(i) Relation of L for C being set for y being Element of L holds SetBelow (R,C,y) is_<=_than y let R be auxiliary(i) Relation of L; ::_thesis: for C being set for y being Element of L holds SetBelow (R,C,y) is_<=_than y let C be set ; ::_thesis: for y being Element of L holds SetBelow (R,C,y) is_<=_than y let y be Element of L; ::_thesis: SetBelow (R,C,y) is_<=_than y let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in SetBelow (R,C,y) or b <= y ) assume b in SetBelow (R,C,y) ; ::_thesis: b <= y then [b,y] in R by Th15; hence b <= y by WAYBEL_4:def_3; ::_thesis: verum end; theorem Th17: :: WAYBEL35:17 for L being reflexive transitive RelStr for R being auxiliary(ii) Relation of L for C being Subset of L for x, y being Element of L st x <= y holds SetBelow (R,C,x) c= SetBelow (R,C,y) proof let L be reflexive transitive RelStr ; ::_thesis: for R being auxiliary(ii) Relation of L for C being Subset of L for x, y being Element of L st x <= y holds SetBelow (R,C,x) c= SetBelow (R,C,y) let R be auxiliary(ii) Relation of L; ::_thesis: for C being Subset of L for x, y being Element of L st x <= y holds SetBelow (R,C,x) c= SetBelow (R,C,y) let C be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds SetBelow (R,C,x) c= SetBelow (R,C,y) let x, y be Element of L; ::_thesis: ( x <= y implies SetBelow (R,C,x) c= SetBelow (R,C,y) ) assume A1: x <= y ; ::_thesis: SetBelow (R,C,x) c= SetBelow (R,C,y) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SetBelow (R,C,x) or a in SetBelow (R,C,y) ) assume A2: a in SetBelow (R,C,x) ; ::_thesis: a in SetBelow (R,C,y) then reconsider L = L as non empty reflexive RelStr ; reconsider a = a as Element of L by A2; A3: a in C by A2, Th15; A4: a <= a ; [a,x] in R by A2, Th15; then [a,y] in R by A4, A1, WAYBEL_4:def_4; hence a in SetBelow (R,C,y) by A3, Th15; ::_thesis: verum end; theorem Th18: :: WAYBEL35:18 for L being RelStr for R being auxiliary(i) Relation of L for C being set for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds x = sup (SetBelow (R,C,x)) proof let L be RelStr ; ::_thesis: for R being auxiliary(i) Relation of L for C being set for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds x = sup (SetBelow (R,C,x)) let R be auxiliary(i) Relation of L; ::_thesis: for C being set for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds x = sup (SetBelow (R,C,x)) let C be set ; ::_thesis: for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds x = sup (SetBelow (R,C,x)) let x be Element of L; ::_thesis: ( x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L implies x = sup (SetBelow (R,C,x)) ) assume that A1: x in C and A2: [x,x] in R and A3: ex_sup_of SetBelow (R,C,x),L ; ::_thesis: x = sup (SetBelow (R,C,x)) A4: for a being Element of L st SetBelow (R,C,x) is_<=_than a holds x <= a proof let a be Element of L; ::_thesis: ( SetBelow (R,C,x) is_<=_than a implies x <= a ) assume A5: SetBelow (R,C,x) is_<=_than a ; ::_thesis: x <= a x in SetBelow (R,C,x) by A1, A2, Th15; hence x <= a by A5, LATTICE3:def_9; ::_thesis: verum end; SetBelow (R,C,x) is_<=_than x by Th16; hence x = sup (SetBelow (R,C,x)) by A4, A3, YELLOW_0:def_9; ::_thesis: verum end; definition let L be RelStr ; let C be Subset of L; attrC is sup-closed means :Def9: :: WAYBEL35:def 9 for X being Subset of C st ex_sup_of X,L holds "\/" (X,L) = "\/" (X,(subrelstr C)); end; :: deftheorem Def9 defines sup-closed WAYBEL35:def_9_:_ for L being RelStr for C being Subset of L holds ( C is sup-closed iff for X being Subset of C st ex_sup_of X,L holds "\/" (X,L) = "\/" (X,(subrelstr C)) ); theorem Th19: :: WAYBEL35:19 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for p, q being Element of L st p in C & q in C & p < q holds ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) proof let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for p, q being Element of L st p in C & q in C & p < q holds ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R for p, q being Element of L st p in C & q in C & p < q holds ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) let C be satisfying_SIC strict_chain of R; ::_thesis: for p, q being Element of L st p in C & q in C & p < q holds ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) let p, q be Element of L; ::_thesis: ( p in C & q in C & p < q implies ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) ) assume that A1: p in C and A2: q in C and A3: p < q ; ::_thesis: ex y being Element of L st ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) A4: R satisfies_SIC_on C by Def7; not q <= p by A3, ORDERS_2:6; then not [q,p] in R by WAYBEL_4:def_3; then [p,q] in R by A1, A2, A3, Def3; then consider w being Element of L such that A5: w in C and A6: [p,w] in R and A7: [w,q] in R and A8: p < w by A1, A2, A3, A4, Th13; consider x1 being Element of L such that A9: x1 in C and [p,x1] in R and A10: [x1,w] in R and A11: p < x1 by A1, A4, A5, A6, A8, Th13; defpred S1[ set , set , set ] means ex b being Element of L st ( \$3 = b & \$3 in C & [\$2,\$3] in R & b <= w ); A12: q <= q ; reconsider D = SetBelow (R,C,w) as non empty set by A9, A10, Th15; reconsider g = x1 as Element of D by A9, A10, Th15; A13: for n being Element of NAT for x being Element of D ex y being Element of D st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of D ex y being Element of D st S1[n,x,y] let x be Element of D; ::_thesis: ex y being Element of D st S1[n,x,y] x in D ; then reconsider t = x as Element of L ; A14: x in C by Th15; A15: [x,w] in R by Th15; percases ( x <> w or x = w ) ; suppose x <> w ; ::_thesis: ex y being Element of D st S1[n,x,y] then consider b being Element of L such that A16: b in C and A17: [x,b] in R and A18: [b,w] in R and t < b by A4, A5, A14, A15, Th13; reconsider y = b as Element of D by A16, A18, Th15; take y ; ::_thesis: S1[n,x,y] take b ; ::_thesis: ( y = b & y in C & [x,y] in R & b <= w ) thus ( y = b & y in C & [x,y] in R & b <= w ) by A16, A17, A18, WAYBEL_4:def_3; ::_thesis: verum end; supposeA19: x = w ; ::_thesis: ex y being Element of D st S1[n,x,y] take x ; ::_thesis: S1[n,x,x] take t ; ::_thesis: ( x = t & x in C & [x,x] in R & t <= w ) thus ( x = t & x in C & [x,x] in R & t <= w ) by A19, Th15; ::_thesis: verum end; end; end; consider f being Function of NAT,D such that A20: f . 0 = g and A21: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A13); reconsider f = f as Function of NAT, the carrier of L by FUNCT_2:7; take y = sup (rng f); ::_thesis: ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) A22: ex_sup_of rng f,L by YELLOW_0:17; A23: dom f = NAT by FUNCT_2:def_1; then x1 <= y by A20, A22, FUNCT_1:3, YELLOW_4:1; hence p < y by A11, ORDERS_2:7; ::_thesis: ( [y,q] in R & y = sup (SetBelow (R,C,y)) ) rng f is_<=_than w proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in rng f or x <= w ) assume x in rng f ; ::_thesis: x <= w then consider n being set such that A24: n in dom f and A25: f . n = x by FUNCT_1:def_3; reconsider n = n as Element of NAT by A24; A26: ex b being Element of L st ( f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A21; then x <= f . (n + 1) by A25, WAYBEL_4:def_3; hence x <= w by A26, ORDERS_2:3; ::_thesis: verum end; then y <= w by A22, YELLOW_0:def_9; hence [y,q] in R by A7, A12, WAYBEL_4:def_4; ::_thesis: y = sup (SetBelow (R,C,y)) A27: ex_sup_of SetBelow (R,C,y),L by YELLOW_0:17; A28: for x being Element of L st SetBelow (R,C,y) is_<=_than x holds y <= x proof let x be Element of L; ::_thesis: ( SetBelow (R,C,y) is_<=_than x implies y <= x ) assume A29: SetBelow (R,C,y) is_<=_than x ; ::_thesis: y <= x rng f is_<=_than x proof defpred S2[ Nat] means f . \$1 in C; let m be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not m in rng f or m <= x ) assume m in rng f ; ::_thesis: m <= x then consider n being set such that A30: n in dom f and A31: f . n = m by FUNCT_1:def_3; reconsider n = n as Element of NAT by A30; A32: f . n <= f . n ; A33: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) k is Element of NAT by ORDINAL1:def_12; then ex b being Element of L st ( f . (k + 1) = b & f . (k + 1) in C & [(f . k),(f . (k + 1))] in R & b <= w ) by A21; hence ( S2[k] implies S2[k + 1] ) ; ::_thesis: verum end; A34: S2[ 0 ] by A9, A20; for n being Nat holds S2[n] from NAT_1:sch_2(A34, A33); then A35: f . n in C ; A36: ex b being Element of L st ( f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A21; f . (n + 1) <= y by A22, A23, FUNCT_1:3, YELLOW_4:1; then [m,y] in R by A31, A36, A32, WAYBEL_4:def_4; then m in SetBelow (R,C,y) by A31, A35, Th15; hence m <= x by A29, LATTICE3:def_9; ::_thesis: verum end; hence y <= x by A22, YELLOW_0:def_9; ::_thesis: verum end; SetBelow (R,C,y) is_<=_than y by Th16; hence y = sup (SetBelow (R,C,y)) by A28, A27, YELLOW_0:def_9; ::_thesis: verum end; theorem :: WAYBEL35:20 for L being non empty lower-bounded Poset for R being extra-order Relation of L for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) proof let L be non empty lower-bounded Poset; ::_thesis: for R being extra-order Relation of L for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) let R be extra-order Relation of L; ::_thesis: for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) let C be non empty strict_chain of R; ::_thesis: ( C is sup-closed & ( for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C implies for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) ) assume that A1: C is sup-closed and A2: for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L ; ::_thesis: ( not R satisfies_SIC_on C or for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) ) assume A3: R satisfies_SIC_on C ; ::_thesis: for c being Element of L st c in C holds c = sup (SetBelow (R,C,c)) let c be Element of L; ::_thesis: ( c in C implies c = sup (SetBelow (R,C,c)) ) assume A4: c in C ; ::_thesis: c = sup (SetBelow (R,C,c)) A5: ex_sup_of SetBelow (R,C,c),L by A2, A4; set d = sup (SetBelow (R,C,c)); SetBelow (R,C,c) c= C by XBOOLE_1:17; then sup (SetBelow (R,C,c)) = "\/" ((SetBelow (R,C,c)),(subrelstr C)) by A1, A5, Def9; then sup (SetBelow (R,C,c)) in the carrier of (subrelstr C) ; then A6: sup (SetBelow (R,C,c)) in C by YELLOW_0:def_15; percases ( c = sup (SetBelow (R,C,c)) or c <> sup (SetBelow (R,C,c)) ) ; suppose c = sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c)) hence c = sup (SetBelow (R,C,c)) ; ::_thesis: verum end; supposeA7: c <> sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c)) A8: now__::_thesis:_(_c_<_sup_(SetBelow_(R,C,c))_implies_c_=_sup_(SetBelow_(R,C,c))_) assume A9: c < sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c)) A10: for a being Element of L st SetBelow (R,C,c) is_<=_than a holds c <= a proof let a be Element of L; ::_thesis: ( SetBelow (R,C,c) is_<=_than a implies c <= a ) assume SetBelow (R,C,c) is_<=_than a ; ::_thesis: c <= a then A11: sup (SetBelow (R,C,c)) <= a by A5, YELLOW_0:def_9; c <= sup (SetBelow (R,C,c)) by A9, ORDERS_2:def_6; hence c <= a by A11, ORDERS_2:3; ::_thesis: verum end; SetBelow (R,C,c) is_<=_than c by Th16; hence c = sup (SetBelow (R,C,c)) by A10, A5, YELLOW_0:def_9; ::_thesis: verum end; ( [c,(sup (SetBelow (R,C,c)))] in R or [(sup (SetBelow (R,C,c))),c] in R ) by A7, A4, A6, Def3; then ( c <= sup (SetBelow (R,C,c)) or [(sup (SetBelow (R,C,c))),c] in R ) by WAYBEL_4:def_3; then consider y being Element of L such that A12: y in C and [(sup (SetBelow (R,C,c))),y] in R and A13: [y,c] in R and A14: sup (SetBelow (R,C,c)) < y by A8, A3, A4, A6, A7, Th13, ORDERS_2:def_6; y in SetBelow (R,C,c) by A12, A13, Th15; hence c = sup (SetBelow (R,C,c)) by A5, A14, ORDERS_2:6, YELLOW_4:1; ::_thesis: verum end; end; end; theorem :: WAYBEL35:21 for L being non empty reflexive antisymmetric RelStr 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 proof 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; percases ( 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 ) ) ; supposeA7: 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 ) reconsider x = x as Element of L ; A8: SetBelow (R,C,z) is_<=_than x proof 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; percases ( x <> b or x = b ) ; supposeA11: x <> b ; ::_thesis: b <= x b in C by A9, Th15; then A12: ( [x,b] in R or x = b or [b,x] in R ) by A2, Def3; not x <= b by A11, A10, ORDERS_2:def_6; hence b <= x by A12, WAYBEL_4:def_3; ::_thesis: verum end; suppose x = b ; ::_thesis: b <= x hence b <= x ; ::_thesis: verum end; end; end; A13: for a being Element of L st SetBelow (R,C,z) is_<=_than a holds x <= a proof A14: x in SetBelow (R,C,z) by A2, A4, Th15; let a be Element of L; ::_thesis: ( SetBelow (R,C,z) is_<=_than a implies x <= a ) assume SetBelow (R,C,z) is_<=_than a ; ::_thesis: x <= a hence x <= a by A14, LATTICE3:def_9; ::_thesis: verum end; 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; 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 ) then consider y being Element of L such that A15: y in SetBelow (R,C,z) and A16: x < y ; take y ; ::_thesis: ( y in C & [x,y] in R & [y,z] in R & x <> y ) thus y in C by A15, Th15; ::_thesis: ( [x,y] in R & [y,z] in R & x <> y ) hence [x,y] in R by A2, A16, Th2; ::_thesis: ( [y,z] in R & x <> y ) thus [y,z] in R by A15, Th15; ::_thesis: x <> y thus x <> y by A16; ::_thesis: verum end; end; end; definition let L be non empty RelStr ; let R be Relation of the carrier of L; let C be set ; defpred S1[ set ] means \$1 = sup (SetBelow (R,C,\$1)); func SupBelow (R,C) -> set means :Def10: :: WAYBEL35:def 10 for y being set holds ( y in it iff y = sup (SetBelow (R,C,y)) ); existence ex b1 being set st for y being set holds ( y in b1 iff y = sup (SetBelow (R,C,y)) ) proof consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for y being set holds ( y in X iff y = sup (SetBelow (R,C,y)) ) thus for y being set holds ( y in X iff y = sup (SetBelow (R,C,y)) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff y = sup (SetBelow (R,C,y)) ) ) & ( for y being set holds ( y in b2 iff y = sup (SetBelow (R,C,y)) ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def10 defines SupBelow WAYBEL35:def_10_:_ for L being non empty RelStr for R being Relation of the carrier of L for C being set for b4 being set holds ( b4 = SupBelow (R,C) iff for y being set holds ( y in b4 iff y = sup (SetBelow (R,C,y)) ) ); definition let L be non empty RelStr ; let R be Relation of the carrier of L; let C be set ; :: original: SupBelow redefine func SupBelow (R,C) -> Subset of L; coherence SupBelow (R,C) is Subset of L proof SupBelow (R,C) c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SupBelow (R,C) or x in the carrier of L ) assume x in SupBelow (R,C) ; ::_thesis: x in the carrier of L then x = sup (SetBelow (R,C,x)) by Def10; hence x in the carrier of L ; ::_thesis: verum end; hence SupBelow (R,C) is Subset of L ; ::_thesis: verum end; end; theorem Th22: :: WAYBEL35:22 for L being non empty reflexive transitive RelStr for R being auxiliary(i) auxiliary(ii) Relation of L for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is strict_chain of R proof let L be non empty reflexive transitive RelStr ; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is strict_chain of R let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is strict_chain of R let C be strict_chain of R; ::_thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is strict_chain of R ) assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; ::_thesis: SupBelow (R,C) is strict_chain of R thus SupBelow (R,C) is strict_chain of R ::_thesis: verum proof let a, b be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in SupBelow (R,C) & b in SupBelow (R,C) & not [a,b] in R & not a = b implies [b,a] in R ) assume A2: a in SupBelow (R,C) ; ::_thesis: ( not b in SupBelow (R,C) or [a,b] in R or a = b or [b,a] in R ) then A3: a = sup (SetBelow (R,C,a)) by Def10; reconsider a = a as Element of L by A2; A4: a <= a ; A5: ex_sup_of SetBelow (R,C,a),L by A1; assume A6: b in SupBelow (R,C) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) then A7: b = sup (SetBelow (R,C,b)) by Def10; reconsider b = b as Element of L by A6; A8: b <= b ; A9: ex_sup_of SetBelow (R,C,b),L by A1; percases ( a = b or a <> b ) ; suppose a = 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 ) ; ::_thesis: verum end; supposeA10: a <> b ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) ( ( for x being Element of L st x in C holds ( [x,a] in R iff [x,b] in R ) ) implies a = b ) proof assume A11: for x being Element of L st x in C holds ( [x,a] in R iff [x,b] in R ) ; ::_thesis: a = b SetBelow (R,C,a) = SetBelow (R,C,b) proof thus SetBelow (R,C,a) c= SetBelow (R,C,b) :: according to XBOOLE_0:def_10 ::_thesis: SetBelow (R,C,b) c= SetBelow (R,C,a) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetBelow (R,C,a) or x in SetBelow (R,C,b) ) assume A12: x in SetBelow (R,C,a) ; ::_thesis: x in SetBelow (R,C,b) then reconsider x = x as Element of L ; A13: x in C by A12, Th15; [x,a] in R by A12, Th15; then [x,b] in R by A13, A11; hence x in SetBelow (R,C,b) by A13, Th15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetBelow (R,C,b) or x in SetBelow (R,C,a) ) assume A14: x in SetBelow (R,C,b) ; ::_thesis: x in SetBelow (R,C,a) then reconsider x = x as Element of L ; A15: x in C by A14, Th15; [x,b] in R by A14, Th15; then [x,a] in R by A15, A11; hence x in SetBelow (R,C,a) by A15, Th15; ::_thesis: verum end; hence a = b by A2, A7, Def10; ::_thesis: verum end; then consider x being Element of L such that A16: x in C and A17: ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A10; A18: x <= x ; thus ( [a,b] in R or a = b or [b,a] in R ) ::_thesis: verum proof percases ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A17; supposethat A19: [x,a] in R and A20: not [x,b] in R ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) SetBelow (R,C,b) is_<=_than x proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in SetBelow (R,C,b) or y <= x ) assume A21: y in SetBelow (R,C,b) ; ::_thesis: y <= x then [y,b] in R by Th15; then A22: y <= b by WAYBEL_4:def_3; y in C by A21, Th15; then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3; hence y <= x by A18, A20, A22, WAYBEL_4:def_3, WAYBEL_4:def_4; ::_thesis: verum end; then b <= x by A7, A9, YELLOW_0:def_9; hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def_4; ::_thesis: verum end; supposethat A23: not [x,a] in R and A24: [x,b] in R ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R ) SetBelow (R,C,a) is_<=_than x proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in SetBelow (R,C,a) or y <= x ) assume A25: y in SetBelow (R,C,a) ; ::_thesis: y <= x then [y,a] in R by Th15; then A26: y <= a by WAYBEL_4:def_3; y in C by A25, Th15; then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3; hence y <= x by A18, A23, A26, WAYBEL_4:def_3, WAYBEL_4:def_4; ::_thesis: verum end; then a <= x by A3, A5, YELLOW_0:def_9; hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def_4; ::_thesis: verum end; end; end; end; end; end; end; theorem :: WAYBEL35:23 for L being non empty Poset for R being auxiliary(i) auxiliary(ii) Relation of L for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is sup-closed proof let L be non empty Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is sup-closed let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being Subset of L st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds SupBelow (R,C) is sup-closed let C be Subset of L; ::_thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is sup-closed ) assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; ::_thesis: SupBelow (R,C) is sup-closed let X be Subset of (SupBelow (R,C)); :: according to WAYBEL35:def_9 ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) ) set s = "\/" (X,L); assume A2: ex_sup_of X,L ; ::_thesis: "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) A3: ex_sup_of SetBelow (R,C,("\/" (X,L))),L by A1; X is_<=_than sup (SetBelow (R,C,("\/" (X,L)))) proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= sup (SetBelow (R,C,("\/" (X,L)))) ) A4: ex_sup_of SetBelow (R,C,x),L by A1; assume A5: x in X ; ::_thesis: x <= sup (SetBelow (R,C,("\/" (X,L)))) then A6: x = sup (SetBelow (R,C,x)) by Def10; SetBelow (R,C,x) c= SetBelow (R,C,("\/" (X,L))) by A2, A5, Th17, YELLOW_4:1; hence x <= sup (SetBelow (R,C,("\/" (X,L)))) by A3, A6, A4, YELLOW_0:34; ::_thesis: verum end; then A7: "\/" (X,L) <= sup (SetBelow (R,C,("\/" (X,L)))) by A2, YELLOW_0:def_9; A8: the carrier of (subrelstr (SupBelow (R,C))) = SupBelow (R,C) by YELLOW_0:def_15; SetBelow (R,C,("\/" (X,L))) is_<=_than "\/" (X,L) by Th16; then sup (SetBelow (R,C,("\/" (X,L)))) <= "\/" (X,L) by A3, YELLOW_0:def_9; then "\/" (X,L) = sup (SetBelow (R,C,("\/" (X,L)))) by A7, ORDERS_2:2; then "\/" (X,L) in SupBelow (R,C) by Def10; hence "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) by A8, A2, YELLOW_0:64; ::_thesis: verum end; theorem Th24: :: WAYBEL35:24 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for d being Element of L st d in SupBelow (R,C) holds d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) proof let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for d being Element of L st d in SupBelow (R,C) holds d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R for d being Element of L st d in SupBelow (R,C) holds d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) let C be satisfying_SIC strict_chain of R; ::_thesis: for d being Element of L st d in SupBelow (R,C) holds d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) let d be Element of L; ::_thesis: ( d in SupBelow (R,C) implies d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) ) deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,\$1] in R ) } ; set p = "\/" (H1(d),L); A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17; A2: H1(d) is_<=_than d proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in H1(d) or a <= d ) assume a in H1(d) ; ::_thesis: a <= d then ex b being Element of L st ( a = b & b in SupBelow (R,C) & [b,d] in R ) ; hence a <= d by WAYBEL_4:def_3; ::_thesis: verum end; assume d in SupBelow (R,C) ; ::_thesis: d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) then A3: d = sup (SetBelow (R,C,d)) by Def10; assume A4: "\/" (H1(d),L) <> d ; ::_thesis: contradiction ex_sup_of H1(d),L by YELLOW_0:17; then "\/" (H1(d),L) <= d by A2, YELLOW_0:def_9; then A5: "\/" (H1(d),L) < d by A4, ORDERS_2:def_6; now__::_thesis:_ex_a_being_Element_of_L_st_ (_a_in_C_&_[a,d]_in_R_&_not_a_<=_"\/"_(H1(d),L)_) percases ( not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) or ex a being Element of L st ( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) ) by A3, A1, A4, YELLOW_0:def_9; suppose not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) ; ::_thesis: ex a being Element of L st ( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) then consider a being Element of L such that A6: a in SetBelow (R,C,d) and A7: not a <= "\/" (H1(d),L) by LATTICE3:def_9; A8: [a,d] in R by A6, Th15; a in C by A6, Th15; hence ex a being Element of L st ( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) by A8, A7; ::_thesis: verum end; suppose ex a being Element of L st ( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) ; ::_thesis: ex a being Element of L st ( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) then consider a being Element of L such that A9: SetBelow (R,C,d) is_<=_than a and A10: not "\/" (H1(d),L) <= a ; d <= a by A3, A1, A9, YELLOW_0:def_9; then "\/" (H1(d),L) < a by A5, ORDERS_2:7; hence ex a being Element of L st ( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) by A10, ORDERS_2:def_6; ::_thesis: verum end; end; end; then consider cc being Element of L such that A11: cc in C and A12: [cc,d] in R and A13: not cc <= "\/" (H1(d),L) ; percases ( [cc,cc] in R or not [cc,cc] in R ) ; suppose [cc,cc] in R ; ::_thesis: contradiction then cc = sup (SetBelow (R,C,cc)) by A11, Th18, YELLOW_0:17; then cc in SupBelow (R,C) by Def10; then cc in H1(d) by A12; hence contradiction by A13, YELLOW_0:17, YELLOW_4:1; ::_thesis: verum end; supposeA14: not [cc,cc] in R ; ::_thesis: contradiction ex cs being Element of L st ( cs in C & cc < cs & [cs,d] in R ) proof percases ( not SetBelow (R,C,d) is_<=_than cc or ex a being Element of L st ( SetBelow (R,C,d) is_<=_than a & not cc <= a ) ) by A3, A1, A12, A14, YELLOW_0:def_9; suppose not SetBelow (R,C,d) is_<=_than cc ; ::_thesis: ex cs being Element of L st ( cs in C & cc < cs & [cs,d] in R ) then consider cs being Element of L such that A15: cs in SetBelow (R,C,d) and A16: not cs <= cc by LATTICE3:def_9; take cs ; ::_thesis: ( cs in C & cc < cs & [cs,d] in R ) A17: not [cs,cc] in R by A16, WAYBEL_4:def_3; thus cs in C by A15, Th15; ::_thesis: ( cc < cs & [cs,d] in R ) then [cc,cs] in R by A17, A11, A16, Def3; then cc <= cs by WAYBEL_4:def_3; hence cc < cs by A16, ORDERS_2:def_6; ::_thesis: [cs,d] in R thus [cs,d] in R by A15, Th15; ::_thesis: verum end; supposeA18: ex a being Element of L st ( SetBelow (R,C,d) is_<=_than a & not cc <= a ) ; ::_thesis: ex cs being Element of L st ( cs in C & cc < cs & [cs,d] in R ) cc in SetBelow (R,C,d) by A11, A12, Th15; hence ex cs being Element of L st ( cs in C & cc < cs & [cs,d] in R ) by A18, LATTICE3:def_9; ::_thesis: verum end; end; end; then consider cs being Element of L such that A19: cs in C and A20: cc < cs and A21: [cs,d] in R ; consider y being Element of L such that A22: cc < y and A23: [y,cs] in R and A24: y = sup (SetBelow (R,C,y)) by A11, A19, A20, Th19; A25: y in SupBelow (R,C) by A24, Def10; A26: d <= d ; y <= cs by A23, WAYBEL_4:def_3; then [y,d] in R by A21, A26, WAYBEL_4:def_4; then y in H1(d) by A25; then y <= "\/" (H1(d),L) by YELLOW_0:17, YELLOW_4:1; then cc < "\/" (H1(d),L) by A22, ORDERS_2:7; hence contradiction by A13, ORDERS_2:def_6; ::_thesis: verum end; end; end; theorem :: WAYBEL35:25 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C) proof let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C) let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C) let C be satisfying_SIC strict_chain of R; ::_thesis: R satisfies_SIC_on SupBelow (R,C) let c, d be Element of L; :: according to WAYBEL35:def_6 ::_thesis: ( c in SupBelow (R,C) & d in SupBelow (R,C) & [c,d] in R & c <> d implies ex y being Element of L st ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) ) assume that A1: c in SupBelow (R,C) and A2: d in SupBelow (R,C) and A3: [c,d] in R and A4: c <> d ; ::_thesis: ex y being Element of L st ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) A5: c <= d by A3, WAYBEL_4:def_3; deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,\$1] in R ) } ; A6: d = "\/" (H1(d),L) by A2, Th24; A7: ex_sup_of H1(d),L by YELLOW_0:17; percases ( not H1(d) is_<=_than c or ex g being Element of L st ( H1(d) is_<=_than g & not c <= g ) ) by A4, A6, A7, YELLOW_0:def_9; suppose not H1(d) is_<=_than c ; ::_thesis: ex y being Element of L st ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) then consider g being Element of L such that A8: g in H1(d) and A9: not g <= c by LATTICE3:def_9; consider y being Element of L such that A10: g = y and A11: y in SupBelow (R,C) and A12: [y,d] in R by A8; reconsider y = y as Element of L ; take y ; ::_thesis: ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) thus y in SupBelow (R,C) by A11; ::_thesis: ( [c,y] in R & [y,d] in R & c <> y ) for c being Element of L holds ex_sup_of SetBelow (R,C,c),L by YELLOW_0:17; then SupBelow (R,C) is strict_chain of R by Th22; then ( [c,y] in R or c = y or [y,c] in R ) by A1, A11, Def3; hence [c,y] in R by A9, A10, WAYBEL_4:def_3; ::_thesis: ( [y,d] in R & c <> y ) thus [y,d] in R by A12; ::_thesis: c <> y thus c <> y by A9, A10; ::_thesis: verum end; suppose ex g being Element of L st ( H1(d) is_<=_than g & not c <= g ) ; ::_thesis: ex y being Element of L st ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) then consider g being Element of L such that A13: H1(d) is_<=_than g and A14: not c <= g ; d <= g by A6, A7, A13, YELLOW_0:def_9; hence ex y being Element of L st ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) by A5, A14, ORDERS_2:3; ::_thesis: verum end; end; end; theorem :: WAYBEL35:26 for L being non empty complete Poset for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for a, b being Element of L st a in C & b in C & a < b holds ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) proof let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L for C being satisfying_SIC strict_chain of R for a, b being Element of L st a in C & b in C & a < b holds ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R for a, b being Element of L st a in C & b in C & a < b holds ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) let C be satisfying_SIC strict_chain of R; ::_thesis: for a, b being Element of L st a in C & b in C & a < b holds ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) let a, b be Element of L; ::_thesis: ( a in C & b in C & a < b implies ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) ) assume that A1: a in C and A2: b in C and A3: a < b ; ::_thesis: ex d being Element of L st ( d in SupBelow (R,C) & a < d & [d,b] in R ) consider d being Element of L such that A4: a < d and A5: [d,b] in R and A6: d = sup (SetBelow (R,C,d)) by A1, A2, A3, Th19; take d ; ::_thesis: ( d in SupBelow (R,C) & a < d & [d,b] in R ) thus ( d in SupBelow (R,C) & a < d & [d,b] in R ) by A4, A5, A6, Def10; ::_thesis: verum end;