waybel35.miz



    begin

    

     Lm1: for x,y,X be set st y in ( {x} \/ X) holds y = x or y in X

    proof

      let x,y,X be set;

      assume y in ( {x} \/ X);

      then y in {x} or y in X by XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    begin

    registration

      let L be RelStr;

      cluster auxiliary(i) for Relation of L;

      existence

      proof

        take ( IntRel L);

        thus thesis;

      end;

    end

    registration

      let L be transitive RelStr;

      cluster auxiliary(i) auxiliary(ii) for Relation of L;

      existence

      proof

        take ( IntRel L);

        thus thesis;

      end;

    end

    registration

      let L be with_suprema antisymmetric RelStr;

      cluster auxiliary(iii) for Relation of L;

      existence

      proof

        take ( IntRel L);

        thus thesis;

      end;

    end

    registration

      let L be non empty lower-bounded antisymmetric RelStr;

      cluster auxiliary(iv) for Relation of L;

      existence

      proof

        take ( IntRel L);

        thus thesis;

      end;

    end

    definition

      let L be non empty RelStr, R be Relation of L;

      :: WAYBEL35:def1

      attr R is extra-order means R is auxiliary(i) auxiliary(ii) auxiliary(iv);

    end

    registration

      let L be non empty RelStr;

      cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for Relation of L;

      coherence ;

      cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for Relation of L;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster extra-order auxiliary(iii) -> auxiliary for Relation of L;

      coherence ;

      cluster auxiliary -> extra-order for Relation of L;

      coherence ;

    end

    registration

      let L be lower-bounded antisymmetric transitive non empty RelStr;

      cluster extra-order for Relation of L;

      existence

      proof

        take ( IntRel L);

        thus thesis;

      end;

    end

    definition

      let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;

      :: WAYBEL35:def2

      func R -LowerMap -> Function of L, ( InclPoset ( LOWER L)) means

      : Def2: for x be Element of L holds (it . x) = (R -below x);

      existence

      proof

        deffunc F( Element of L) = (R -below $1);

        

         A1: for x be Element of L holds F(x) is Element of ( InclPoset ( LOWER L))

        proof

          let x be Element of L;

          reconsider I = F(x) as lower Subset of L;

          ( LOWER L) = { X where X be Subset of L : X is lower } by LATTICE7:def 7;

          then I in ( LOWER L);

          hence thesis by YELLOW_1: 1;

        end;

        consider f be Function of L, ( InclPoset ( LOWER L)) such that

         A2: for x be Element of L holds (f . x) = F(x) from FUNCT_2:sch 9( A1);

        take f;

        let x be Element of L;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let M1,M2 be Function of L, ( InclPoset ( LOWER L));

        assume

         A3: for x be Element of L holds (M1 . x) = (R -below x);

        assume

         A4: for x be Element of L holds (M2 . x) = (R -below x);

        for x be object st x in the carrier of L holds (M1 . x) = (M2 . x)

        proof

          let x be object;

          assume x in the carrier of L;

          then

          reconsider x9 = x as Element of L;

          

          thus (M1 . x) = (R -below x9) by A3

          .= (M2 . x) by A4;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    registration

      let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;

      cluster (R -LowerMap ) -> monotone;

      coherence

      proof

        let x,y be Element of L;

        set s = (R -LowerMap );

        

         A1: (s . y) = (R -below y) by Def2;

        assume x <= y;

        then

         A2: (R -below x) c= (R -below y) by WAYBEL_4: 17;

        (s . x) = (R -below x) by Def2;

        hence thesis by A2, A1, YELLOW_1: 3;

      end;

    end

    definition

      let L be 1-sorted, R be Relation of the carrier of L;

      :: WAYBEL35:def3

      mode strict_chain of R -> Subset of L means

      : Def3: for x,y be set st x in it & y in it holds [x, y] in R or x = y or [y, x] in R;

      existence

      proof

        take ( {} L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL35:1

    

     Th1: for L be 1-sorted, C be trivial Subset of L, R be Relation of the carrier of L holds C is strict_chain of R

    proof

      let L be 1-sorted, C be trivial Subset of L, R be Relation of the carrier of L;

      let x,y be set;

      thus thesis by SUBSET_1:def 7;

    end;

    registration

      let L be non empty 1-sorted, R be Relation of the carrier of L;

      cluster 1 -element for strict_chain of R;

      existence

      proof

        set C = the 1 -element Subset of L;

        reconsider C as strict_chain of R by Th1;

        take C;

        thus thesis;

      end;

    end

    theorem :: WAYBEL35:2

    

     Th2: for L be antisymmetric RelStr, R be auxiliary(i) Relation of L, C be strict_chain of R, x,y be Element of L st x in C & y in C & x < y holds [x, y] in R

    proof

      let L be antisymmetric RelStr, R be auxiliary(i) Relation of L, C be strict_chain of R, x,y be Element of L;

      assume that

       A1: x in C and

       A2: y in C and

       A3: x < y;

       [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 thesis by A3, ORDERS_2: 6;

    end;

    theorem :: WAYBEL35:3

    for L be antisymmetric RelStr, R be auxiliary(i) Relation of L, x,y be Element of L st [x, y] in R & [y, x] in R holds x = y

    proof

      let L be antisymmetric RelStr, R be auxiliary(i) Relation of L, x,y be Element of L;

      assume that

       A1: [x, y] in R and

       A2: [y, x] in R;

      

       A3: y <= x by A2, WAYBEL_4:def 3;

      x <= y by A1, WAYBEL_4:def 3;

      hence thesis by A3, ORDERS_2: 2;

    end;

    theorem :: WAYBEL35:4

    for L be non empty lower-bounded antisymmetric RelStr, x be Element of L, R be auxiliary(iv) Relation of L holds {( Bottom L), x} is strict_chain of R

    proof

      let L be non empty lower-bounded antisymmetric RelStr, x be Element of L, R be auxiliary(iv) Relation of L;

      let a,y be set;

      assume that

       A1: a in {( Bottom L), x} and

       A2: y in {( Bottom L), x};

      

       A3: y = ( Bottom L) or y = x by A2, TARSKI:def 2;

      a = ( Bottom L) or a = x by A1, TARSKI:def 2;

      hence thesis by A3, WAYBEL_4:def 6;

    end;

    theorem :: WAYBEL35:5

    

     Th5: for L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) Relation of L, C be strict_chain of R holds (C \/ {( Bottom L)}) is strict_chain of R

    proof

      let L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) Relation of L, C be strict_chain of R;

      set A = (C \/ {( Bottom L)});

      let x,y be set;

      assume that

       A1: x in A and

       A2: y in A;

      reconsider x, y as Element of L by A1, A2;

      per cases by A1, A2, Lm1;

        suppose x in C & y in C;

        hence thesis by Def3;

      end;

        suppose x in C & y = ( Bottom L);

        hence thesis by WAYBEL_4:def 6;

      end;

        suppose x = ( Bottom L) & y in C;

        hence thesis by WAYBEL_4:def 6;

      end;

        suppose x = ( Bottom L) & y = ( Bottom L);

        hence thesis;

      end;

    end;

    definition

      let L be 1-sorted, R be Relation of the carrier of L, C be strict_chain of R;

      :: WAYBEL35:def4

      attr C is maximal means for D be strict_chain of R st C c= D holds C = D;

    end

    definition

      let L be 1-sorted, R be Relation of the carrier of L, C be set;

      defpred P[ set] means $1 is strict_chain of R & C c= $1;

      :: WAYBEL35:def5

      func Strict_Chains (R,C) -> set means

      : Def5: for x be set holds x in it iff x is strict_chain of R & C c= x;

      existence

      proof

        consider X be set such that

         A1: for x be set holds x in X iff x in ( bool the carrier of L) & P[x] from XFAMILY:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        thus for X1,X2 be set st (for x be set holds x in X1 iff P[x]) & (for x be set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;

      end;

    end

    registration

      let L be 1-sorted, R be Relation of the carrier of L, C be strict_chain of R;

      cluster ( Strict_Chains (R,C)) -> non empty;

      coherence by Def5;

    end

    notation

      let R be Relation, X be set;

      synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;

    end

    theorem :: WAYBEL35:6

    for L be 1-sorted, R be Relation of the carrier of L, C be strict_chain of R holds ( Strict_Chains (R,C)) is_inductive_wrt ( RelIncl ( Strict_Chains (R,C))) & ex D be set st D is_maximal_in ( RelIncl ( Strict_Chains (R,C))) & C c= D

    proof

      let L be 1-sorted, R be Relation of the carrier of L, C be strict_chain of R;

      set X = ( Strict_Chains (R,C));

      

       A1: ( field ( RelIncl X)) = X by WELLORD2:def 1;

      thus

       A2: X is_inductive_wrt ( RelIncl X)

      proof

        let Y be set such that

         A3: Y c= X and

         A4: (( RelIncl X) |_2 Y) is being_linear-order;

        per cases ;

          suppose

           A5: Y is empty;

          take C;

          thus thesis by A5, Def5;

        end;

          suppose

           A6: Y is non empty;

          take Z = ( union Y);

          Z c= the carrier of L

          proof

            let z be object;

            assume z in Z;

            then

            consider A be 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 thesis by A7;

          end;

          then

          reconsider S = Z as Subset of L;

          

           A9: S is strict_chain of R

          proof

            (( RelIncl X) |_2 Y) is connected by A4;

            then

             A10: (( RelIncl X) |_2 Y) is_connected_in ( field (( RelIncl X) |_2 Y)) by RELAT_2:def 14;

            

             A11: (( RelIncl X) |_2 Y) = ( RelIncl Y) by A3, WELLORD2: 7;

            let x,y be set;

            

             A12: ( field ( RelIncl Y)) = Y by WELLORD2:def 1;

            assume x in S;

            then

            consider A be 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;

            then

            consider B be 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;

            per cases ;

              suppose A <> B;

              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 thesis by A13, A16, A15, A18, Def3;

            end;

              suppose A = B;

              hence thesis by A13, A16, A15, Def3;

            end;

          end;

          C c= Z

          proof

            let c be object;

            assume

             A19: c in C;

            consider y be object such that

             A20: y in Y by A6;

            reconsider y as set by TARSKI: 1;

            C c= y by A3, A20, Def5;

            hence thesis by A19, A20, TARSKI:def 4;

          end;

          hence

           A21: Z in X by A9, Def5;

          let y be set;

          assume

           A22: y in Y;

          then y c= Z by ZFMISC_1: 74;

          hence thesis by A3, A21, A22, WELLORD2:def 1;

        end;

      end;

      

       A23: ( RelIncl X) is_transitive_in X by WELLORD2: 20;

      

       A24: ( RelIncl X) is_antisymmetric_in X by WELLORD2: 21;

      ( RelIncl X) is_reflexive_in X by WELLORD2: 19;

      then ( RelIncl X) partially_orders X by A23, A24;

      then

      consider D be set such that

       A25: D is_maximal_in ( RelIncl X) by A1, A2, ORDERS_1: 63;

      take D;

      thus D is_maximal_in ( RelIncl X) by A25;

      D in ( field ( RelIncl X)) by A25;

      hence thesis by A1, Def5;

    end;

    theorem :: WAYBEL35:7

    

     Th7: for L be non empty transitive RelStr, C be non empty Subset of L, X be 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, C be non empty Subset of L, X be Subset of C such that

       A1: ex_sup_of (X,L) and

       A2: ( "\/" (X,L)) in C;

      the carrier of ( subrelstr C) = C by YELLOW_0:def 15;

      hence thesis by A1, A2, YELLOW_0: 64;

    end;

    

     Lm2: for L be non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be Subset of C st ex_sup_of (X,L) & C is maximal & not ( "\/" (X,L)) in C holds ex cs be Element of L st cs in C & ( "\/" (X,L)) < cs & not [( "\/" (X,L)), cs] in R & ex cs1 be Element of ( subrelstr C) st cs = cs1 & X is_<=_than cs1 & for a be Element of ( subrelstr C) st X is_<=_than a holds cs1 <= a

    proof

      let L be non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be Subset of C such that

       A1: ex_sup_of (X,L) and

       A2: C is maximal;

      set s = ( "\/" (X,L));

      

       A3: C c= (C \/ {s}) by XBOOLE_1: 7;

      assume

       A4: not s in C;

      then not (C \/ {s}) c= C by ZFMISC_1: 39;

      then

       A5: not (C \/ {s}) is strict_chain of R by A3, A2;

      ex cs be Element of L st cs in C & s < cs & not [s, cs] in R

      proof

        

         A6: for a be Element of L st a in C & not [a, s] in R & not [s, a] in R holds ex cs be Element of L st cs in C & s < cs & not [s, cs] in R

        proof

          let a be Element of L;

          assume that

           A7: a in C and

           A8: not [a, s] in R and

           A9: not [s, a] in R;

          take a;

          thus a in C by A7;

          a is_>=_than X

          proof

            let x be Element of L;

            assume

             A10: x in X;

            per cases by A7, A10, Def3;

              suppose

               A11: [a, x] in R;

              

               A12: a <= a;

              x <= s by A1, A10, YELLOW_4: 1;

              hence x <= a by A12, A8, A11, WAYBEL_4:def 4;

            end;

              suppose [x, a] in R or a = x;

              hence x <= a by WAYBEL_4:def 3;

            end;

          end;

          then s <= a by A1, YELLOW_0:def 9;

          hence s < a by A4, A7, ORDERS_2:def 6;

          thus thesis by A9;

        end;

        consider a,b be set such that

         A13: a in (C \/ {s}) and

         A14: b in (C \/ {s}) and

         A15: not [a, b] in R and

         A16: a <> b and

         A17: not [b, a] in R by A5, Def3;

        reconsider a, b as Element of L by A13, A14;

        per cases by A13, A14, Lm1;

          suppose a in C & b in C;

          hence thesis by A15, A16, A17, Def3;

        end;

          suppose a in C & b = s;

          hence thesis by A15, A17, A6;

        end;

          suppose a = s & b in C;

          hence thesis by A15, A17, A6;

        end;

          suppose a = s & b = s;

          hence thesis by A16;

        end;

      end;

      then

      consider cs be Element of L such that

       A18: cs in C and

       A19: s < cs and

       A20: not [s, cs] in R;

      take cs;

      thus cs in C & s < cs & not [s, cs] in R by A18, A19, A20;

      reconsider cs1 = cs as Element of ( subrelstr C) by A18, YELLOW_0:def 15;

      take cs1;

      thus cs = cs1;

      

       A21: s <= cs by A19, ORDERS_2:def 6;

      thus X is_<=_than cs1

      proof

        let b be Element of ( subrelstr C);

        reconsider b0 = b as Element of L by YELLOW_0: 58;

        assume b in X;

        then b0 <= s by A1, YELLOW_4: 1;

        then b0 <= cs by A21, ORDERS_2: 3;

        hence b <= cs1 by YELLOW_0: 60;

      end;

      let a be Element of ( subrelstr C);

      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;

      then X is_<=_than a0 by A22, YELLOW_0: 62;

      then

       A23: s <= 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 thesis by YELLOW_0: 60;

    end;

    theorem :: WAYBEL35:8

    

     Th8: for L be non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be 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, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be Subset of C;

      assume that

       A1: ex_sup_of (X,L) and

       A2: C is maximal;

      set s = ( "\/" (X,L));

      per cases ;

        suppose s in C;

        hence thesis by A1, Th7;

      end;

        suppose not s in C;

        then ex cs be Element of L st cs in C & s < cs & not [s, cs] in R & ex cs1 be Element of ( subrelstr C) st cs = cs1 & X is_<=_than cs1 & for a be Element of ( subrelstr C) st X is_<=_than a holds cs1 <= a by A1, A2, Lm2;

        hence thesis by YELLOW_0: 15;

      end;

    end;

    theorem :: WAYBEL35:9

    for L be non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be 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, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R, X be Subset of C;

      set s = ( "\/" (X,L)), x = ( "\/" (X,( subrelstr C))), U = ( uparrow s);

      assume that

       A1: ex_inf_of ((U /\ C),L) and

       A2: ex_sup_of (X,L) and

       A3: C is maximal;

      

       A4: s <= s;

      reconsider x1 = x as Element of L by YELLOW_0: 58;

      

       A5: the carrier of ( subrelstr C) = C by YELLOW_0:def 15;

      per cases ;

        suppose

         A6: s in C;

        then

         A7: s = x by A2, A5, YELLOW_0: 64;

        

         A8: (U /\ C) is_>=_than x1

        proof

          let b be Element of L;

          assume b in (U /\ C);

          then b in U by XBOOLE_0:def 4;

          hence x1 <= b by A7, WAYBEL_0: 18;

        end;

        for a be Element of L st (U /\ C) is_>=_than a holds a <= x1

        proof

          s in U by A4, WAYBEL_0: 18;

          then

           A9: x1 in (U /\ C) by A6, A7, XBOOLE_0:def 4;

          let a be Element of L;

          assume (U /\ C) is_>=_than a;

          hence thesis by A9;

        end;

        hence thesis by A1, A6, A8, YELLOW_0:def 10;

      end;

        suppose not s in C;

        then

        consider cs be Element of L such that

         A10: cs in C and

         A11: s < cs and

         A12: not [s, cs] in R and

         A13: ex cs1 be Element of ( subrelstr C) st cs = cs1 & X is_<=_than cs1 & for a be Element of ( subrelstr C) st X is_<=_than a holds cs1 <= a by A2, A3, Lm2;

        

         A14: s <= cs by A11, ORDERS_2:def 6;

        

         A15: for a be Element of L st (U /\ C) is_>=_than a holds a <= cs

        proof

          cs in U by A14, WAYBEL_0: 18;

          then

           A16: cs in (U /\ C) by A10, XBOOLE_0:def 4;

          let a be Element of L;

          assume (U /\ C) is_>=_than a;

          hence thesis by A16;

        end;

        

         A17: cs <= cs;

        

         A18: (U /\ C) is_>=_than cs

        proof

          let b be Element of L;

          assume

           A19: b in (U /\ C);

          then b in U by XBOOLE_0:def 4;

          then

           A20: s <= 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;

        end;

         ex_sup_of (X,( subrelstr C)) by A2, A3, Th8;

        then cs = x by A13, YELLOW_0:def 9;

        hence thesis by A15, A1, A11, A18, YELLOW_0:def 10;

      end;

    end;

    theorem :: WAYBEL35:10

    for L be complete non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R st C is maximal holds ( subrelstr C) is complete

    proof

      let L be complete non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be non empty strict_chain of R;

      assume

       A1: C is maximal;

      for X be Subset of ( subrelstr C) holds ex_sup_of (X,( subrelstr C))

      proof

        let X be Subset of ( subrelstr C);

        X is Subset of C by YELLOW_0:def 15;

        hence thesis by A1, Th8, YELLOW_0: 17;

      end;

      hence thesis by YELLOW_0: 53;

    end;

    theorem :: WAYBEL35:11

    for L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) Relation of L, C be strict_chain of R st C is maximal holds ( Bottom L) in C

    proof

      let L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) Relation of L, C be strict_chain of R such that

       A1: for D be strict_chain of R st C c= D holds C = D;

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

      then not ( Bottom L) in {( Bottom L)} by A2, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: WAYBEL35:12

    for L be non empty upper-bounded Poset, R be auxiliary(ii) Relation of L, C be strict_chain of R, m be 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, R be auxiliary(ii) Relation of L, C be strict_chain of R, m be Element of L such that

       A1: C is maximal and

       A2: m is_maximum_of C and

       A3: [m, ( Top L)] in R;

      

       A4: C c= (C \/ {( Top L)}) by XBOOLE_1: 7;

      now

        

         A5: m <= ( Top L) by YELLOW_0: 45;

        assume

         A6: m <> ( Top L);

        

         A7: {( Top L)} c= (C \/ {( Top L)}) by XBOOLE_1: 7;

        

         A8: ex_sup_of (C,L) by A2;

        

         A9: ( sup C) = m by A2;

        (C \/ {( Top L)}) is strict_chain of R

        proof

          let a,b be set;

          assume that

           A10: a in (C \/ {( Top L)}) and

           A11: b in (C \/ {( Top L)});

          

           A12: ( Top L) <= ( Top L);

          per cases by A10, A11, Lm1;

            suppose a in C & b in C;

            hence thesis by Def3;

          end;

            suppose that

             A13: a = ( Top L) and

             A14: b in C;

            reconsider b as Element of L by A14;

            b <= ( sup C) by A8, A14, YELLOW_4: 1;

            hence thesis by A3, A9, A12, A13, WAYBEL_4:def 4;

          end;

            suppose that

             A15: a in C and

             A16: b = ( Top L);

            reconsider a as Element of L by A15;

            a <= ( sup C) by A8, A15, YELLOW_4: 1;

            hence thesis by A3, A9, A12, A16, WAYBEL_4:def 4;

          end;

            suppose a = ( Top L) & b = ( Top L);

            hence thesis;

          end;

        end;

        then

         A17: (C \/ {( Top L)}) = C by A1, A4;

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

      end;

      hence thesis by A3;

    end;

    definition

      let L be RelStr, C be set, R be Relation of the carrier of L;

      :: WAYBEL35:def6

      pred R satisfies_SIC_on C means for x,z be Element of L holds x in C & z in C & [x, z] in R & x <> z implies ex y be Element of L st y in C & [x, y] in R & [y, z] in R & x <> y;

    end

    definition

      let L be RelStr, R be Relation of the carrier of L, C be strict_chain of R;

      :: WAYBEL35:def7

      attr C is satisfying_SIC means

      : Def7: R satisfies_SIC_on C;

    end

    theorem :: WAYBEL35:13

    

     Th13: for L be RelStr, C be set, R be auxiliary(i) Relation of L st R satisfies_SIC_on C holds for x,z be Element of L holds x in C & z in C & [x, z] in R & x <> z implies ex y be Element of L st y in C & [x, y] in R & [y, z] in R & x < y

    proof

      let L be RelStr, C be set, R be auxiliary(i) Relation of L such that

       A1: R satisfies_SIC_on C;

      let x,z be Element of L;

      assume that

       A2: x in C and

       A3: z in C and

       A4: [x, z] in R and

       A5: x <> z;

      consider y be 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;

      take y;

      thus y in C & [x, y] in R & [y, z] in R by A6, A7, A8;

      x <= y by A7, WAYBEL_4:def 3;

      hence thesis by A9, ORDERS_2:def 6;

    end;

    registration

      let L be RelStr, R be Relation of the carrier of L;

      cluster trivial -> satisfying_SIC for strict_chain of R;

      coherence

      proof

        let C be strict_chain of R;

        assume

         A1: C is trivial;

        let x,z be Element of L;

        assume that

         A2: x in C and

         A3: z in C and [x, z] in R and

         A4: x <> z;

        thus thesis by A2, A3, A4, A1, SUBSET_1:def 7;

      end;

    end

    registration

      let L be non empty RelStr, R be Relation of the carrier of L;

      cluster 1 -element for strict_chain of R;

      existence

      proof

        set C = the 1 -element Subset of L;

        reconsider C as strict_chain of R by Th1;

        take C;

        thus thesis;

      end;

    end

    theorem :: WAYBEL35:14

    for L be lower-bounded with_suprema Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be 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, R be auxiliary(i) auxiliary(ii) Relation of L, C be strict_chain of R such that

       A1: C is maximal and

       A2: R is satisfying_SI;

      let x,z be Element of L;

      assume that

       A3: x in C and

       A4: z in C and

       A5: [x, z] in R and

       A6: x <> z;

      consider y be 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: not thesis;

      

       A12: x <= y by A7, WAYBEL_4:def 3;

      

       A13: (C \/ {y}) is strict_chain of R

      proof

        let a,b be set such that

         A14: a in (C \/ {y}) and

         A15: b in (C \/ {y});

        per cases by A14, A15, Lm1;

          suppose a in C & b in C;

          hence thesis by Def3;

        end;

          suppose that

           A16: a in C and

           A17: b = y;

          now

            reconsider a as Element of L by A16;

            

             A18: a <= a;

            per cases by A11, A16;

              suppose x = a;

              hence thesis by A7, A17;

            end;

              suppose a = z;

              hence thesis by A8, A17;

            end;

              suppose not [x, a] in R & a <> x;

              then [a, x] in R by A3, A16, Def3;

              hence thesis by A12, A17, A18, WAYBEL_4:def 4;

            end;

              suppose not [a, z] in R & a <> z;

              then [z, a] in R by A4, A16, Def3;

              hence thesis by A10, A17, A18, WAYBEL_4:def 4;

            end;

          end;

          hence thesis;

        end;

          suppose that

           A19: a = y and

           A20: b in C;

          now

            reconsider b as Element of L by A20;

            

             A21: b <= b;

            per cases by A11, A20;

              suppose x = b;

              hence thesis by A7, A19;

            end;

              suppose b = z;

              hence thesis by A8, A19;

            end;

              suppose not [x, b] in R & b <> x;

              then [b, x] in R by A3, A20, Def3;

              hence thesis by A12, A19, A21, WAYBEL_4:def 4;

            end;

              suppose not [b, z] in R & b <> z;

              then [z, b] in R by A4, A20, Def3;

              hence thesis by A10, A19, A21, WAYBEL_4:def 4;

            end;

          end;

          hence thesis;

        end;

          suppose a = y & b = y;

          hence thesis;

        end;

      end;

      C c= (C \/ {y}) by XBOOLE_1: 7;

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

      then y in C by ZFMISC_1: 39;

      hence thesis by A11, A7, A8, A9;

    end;

    definition

      let R be Relation, C be set, y be object;

      :: WAYBEL35:def8

      func SetBelow (R,C,y) -> set equals ((R " {y}) /\ C);

      coherence ;

    end

    theorem :: WAYBEL35:15

    

     Th15: for R be Relation, C,x,y be set holds x in ( SetBelow (R,C,y)) iff [x, y] in R & x in C

    proof

      let R be Relation, C,x,y be set;

      hereby

        assume

         A1: x in ( SetBelow (R,C,y));

        then x in (R " {y}) by XBOOLE_0:def 4;

        then ex a be object st [x, a] in R & a in {y} by RELAT_1:def 14;

        hence [x, y] in R by TARSKI:def 1;

        thus x in C by A1, XBOOLE_0:def 4;

      end;

      assume that

       A2: [x, y] in R and

       A3: x in C;

      y in {y} by TARSKI:def 1;

      then x in (R " {y}) by A2, RELAT_1:def 14;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    definition

      let L be 1-sorted, R be Relation of the carrier of L, C be set, y be object;

      :: original: SetBelow

      redefine

      func SetBelow (R,C,y) -> Subset of L ;

      coherence

      proof

        ((R " {y}) /\ C) c= the carrier of L;

        hence thesis;

      end;

    end

    theorem :: WAYBEL35:16

    

     Th16: for L be RelStr, R be auxiliary(i) Relation of L, C be set, y be Element of L holds ( SetBelow (R,C,y)) is_<=_than y

    proof

      let L be RelStr, R be auxiliary(i) Relation of L, C be set, y be Element of L;

      let b be Element of L;

      assume b in ( SetBelow (R,C,y));

      then [b, y] in R by Th15;

      hence thesis by WAYBEL_4:def 3;

    end;

    theorem :: WAYBEL35:17

    

     Th17: for L be reflexive transitive RelStr, R be auxiliary(ii) Relation of L, C be Subset of L, x,y be Element of L st x <= y holds ( SetBelow (R,C,x)) c= ( SetBelow (R,C,y))

    proof

      let L be reflexive transitive RelStr, R be auxiliary(ii) Relation of L, C be Subset of L, x,y be Element of L such that

       A1: x <= y;

      let a be object;

      assume

       A2: a in ( SetBelow (R,C,x));

      then

      reconsider L as non empty reflexive RelStr;

      reconsider 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 thesis by A3, Th15;

    end;

    theorem :: WAYBEL35:18

    

     Th18: for L be RelStr, R be auxiliary(i) Relation of L, C be set, x be 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, R be auxiliary(i) Relation of L, C be set, x be Element of L;

      assume that

       A1: x in C and

       A2: [x, x] in R and

       A3: ex_sup_of (( SetBelow (R,C,x)),L);

      

       A4: for a be Element of L st ( SetBelow (R,C,x)) is_<=_than a holds x <= a by A1, A2, Th15;

      ( SetBelow (R,C,x)) is_<=_than x by Th16;

      hence thesis by A4, A3, YELLOW_0:def 9;

    end;

    definition

      let L be RelStr, C be Subset of L;

      :: WAYBEL35:def9

      attr C is sup-closed means for X be Subset of C st ex_sup_of (X,L) holds ( "\/" (X,L)) = ( "\/" (X,( subrelstr C)));

    end

    theorem :: WAYBEL35:19

    

     Th19: for L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, p,q be Element of L st p in C & q in C & p < q holds ex y be Element of L st p < y & [y, q] in R & y = ( sup ( SetBelow (R,C,y)))

    proof

      let L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, p,q be Element of L such that

       A1: p in C and

       A2: q in C and

       A3: p < q;

      

       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 be 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 be 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 P[ set, set, set] means ex b be 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 be Nat, x be Element of D holds ex y be Element of D st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of D;

        x in D;

        then

        reconsider t = x as Element of L;

        

         A14: x in C by Th15;

        

         A15: [x, w] in R by Th15;

        per cases ;

          suppose x <> w;

          then

          consider b be 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, b;

          thus thesis by A16, A17, A18, WAYBEL_4:def 3;

        end;

          suppose

           A19: x = w;

          take x, t;

          thus thesis by A19, Th15;

        end;

      end;

      consider f be sequence of D such that

       A20: (f . 0 ) = g and

       A21: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A13);

      reconsider f as sequence of the carrier of L by FUNCT_2: 7;

      take y = ( sup ( rng f));

      

       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;

      ( rng f) is_<=_than w

      proof

        let x be Element of L;

        assume x in ( rng f);

        then

        consider n be object such that

         A24: n in ( dom f) and

         A25: (f . n) = x by FUNCT_1:def 3;

        reconsider n as Element of NAT by A24;

        

         A26: ex b be 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 . ( In ((n + 1), NAT ))) by A25, WAYBEL_4:def 3;

        hence x <= w by A26, ORDERS_2: 3;

      end;

      then y <= w by A22, YELLOW_0:def 9;

      hence [y, q] in R by A7, A12, WAYBEL_4:def 4;

      

       A27: ex_sup_of (( SetBelow (R,C,y)),L) by YELLOW_0: 17;

      

       A28: for x be Element of L st ( SetBelow (R,C,y)) is_<=_than x holds y <= x

      proof

        let x be Element of L such that

         A29: ( SetBelow (R,C,y)) is_<=_than x;

        ( rng f) is_<=_than x

        proof

          defpred P[ Nat] means (f . $1) in C;

          let m be Element of L;

          assume m in ( rng f);

          then

          consider n be object such that

           A30: n in ( dom f) and

           A31: (f . n) = m by FUNCT_1:def 3;

          reconsider n as Element of NAT by A30;

          

           A32: (f . n) <= (f . n);

          

           A33: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            ex b be 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 thesis;

          end;

          

           A34: P[ 0 ] by A9, A20;

          for n be Nat holds P[n] from NAT_1:sch 2( A34, A33);

          then

           A35: (f . n) in C;

          

           A36: ex b be 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 . ( In ((n + 1), NAT ))) <= 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;

        end;

        hence thesis by A22, YELLOW_0:def 9;

      end;

      ( SetBelow (R,C,y)) is_<=_than y by Th16;

      hence thesis by A28, A27, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL35:20

    for L be lower-bounded non empty Poset, R be extra-order Relation of L, C be non empty strict_chain of R st C is sup-closed & (for c be Element of L st c in C holds ex_sup_of (( SetBelow (R,C,c)),L)) & R satisfies_SIC_on C holds for c be Element of L st c in C holds c = ( sup ( SetBelow (R,C,c)))

    proof

      let L be lower-bounded non empty Poset, R be extra-order Relation of L, C be non empty strict_chain of R;

      assume that

       A1: C is sup-closed and

       A2: for c be Element of L st c in C holds ex_sup_of (( SetBelow (R,C,c)),L);

      assume

       A3: R satisfies_SIC_on C;

      let c be Element of L such that

       A4: c in 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 d = ( "\/" (( SetBelow (R,C,c)),( subrelstr C))) by A1, A5;

      then d in the carrier of ( subrelstr C);

      then

       A6: d in C by YELLOW_0:def 15;

      per cases ;

        suppose c = d;

        hence thesis;

      end;

        suppose

         A7: c <> d;

         A8:

        now

          assume

           A9: c < d;

          

           A10: for a be Element of L st ( SetBelow (R,C,c)) is_<=_than a holds c <= a

          proof

            let a be Element of L;

            assume ( SetBelow (R,C,c)) is_<=_than a;

            then

             A11: d <= a by A5, YELLOW_0:def 9;

            c <= d by A9, ORDERS_2:def 6;

            hence thesis by A11, ORDERS_2: 3;

          end;

          ( SetBelow (R,C,c)) is_<=_than c by Th16;

          hence thesis by A10, A5, YELLOW_0:def 9;

        end;

         [c, d] in R or [d, c] in R by A7, A4, A6, Def3;

        then c <= d or [d, c] in R by WAYBEL_4:def 3;

        then

        consider y be Element of L such that

         A12: y in C and [d, y] in R and

         A13: [y, c] in R and

         A14: d < y by A8, A3, A4, A6, A7, Th13, ORDERS_2:def 6;

        y in ( SetBelow (R,C,c)) by A12, A13, Th15;

        hence thesis by A5, A14, ORDERS_2: 6, YELLOW_4: 1;

      end;

    end;

    theorem :: WAYBEL35:21

    for L be non empty reflexive antisymmetric RelStr, R be auxiliary(i) Relation of L, C be strict_chain of R st (for c be 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, R be auxiliary(i) Relation of L, C be strict_chain of R;

      assume

       A1: for c be Element of L st c in C holds ex_sup_of (( SetBelow (R,C,c)),L) & c = ( sup ( SetBelow (R,C,c)));

      let x,z be Element of L;

      assume that

       A2: x in C and

       A3: z in C and

       A4: [x, z] in R and

       A5: x <> z;

      

       A6: z = ( sup ( SetBelow (R,C,z))) by A1, A3;

      per cases ;

        suppose

         A7: not ex y be Element of L st y in ( SetBelow (R,C,z)) & x < y;

        reconsider x as Element of L;

        

         A8: ( SetBelow (R,C,z)) is_<=_than x

        proof

          let b be Element of L;

          assume

           A9: b in ( SetBelow (R,C,z));

          then

           A10: not x < b by A7;

          per cases ;

            suppose

             A11: x <> b;

            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;

          end;

            suppose x = b;

            hence b <= x;

          end;

        end;

        

         A13: for a be Element of L st ( SetBelow (R,C,z)) is_<=_than a holds x <= a by A2, A4, Th15;

         ex_sup_of (( SetBelow (R,C,z)),L) by A1, A3;

        hence thesis by A13, A5, A6, A8, YELLOW_0:def 9;

      end;

        suppose ex y be Element of L st y in ( SetBelow (R,C,z)) & x < y;

        then

        consider y be Element of L such that

         A14: y in ( SetBelow (R,C,z)) and

         A15: x < y;

        take y;

        thus y in C by A14, Th15;

        hence [x, y] in R by A2, A15, Th2;

        thus [y, z] in R by A14, Th15;

        thus thesis by A15;

      end;

    end;

    definition

      let L be non empty RelStr, R be Relation of the carrier of L, C be set;

      defpred P[ set] means $1 = ( sup ( SetBelow (R,C,$1)));

      :: WAYBEL35:def10

      func SupBelow (R,C) -> set means

      : Def10: for y be set holds y in it iff y = ( sup ( SetBelow (R,C,y)));

      existence

      proof

        consider X be set such that

         A1: for x be set holds x in X iff x in the carrier of L & P[x] from XFAMILY:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        thus for X1,X2 be set st (for x be set holds x in X1 iff P[x]) & (for x be set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;

      end;

    end

    definition

      let L be non empty RelStr, R be Relation of the carrier of L, C be set;

      :: original: SupBelow

      redefine

      func SupBelow (R,C) -> Subset of L ;

      coherence

      proof

        ( SupBelow (R,C)) c= the carrier of L

        proof

          let x be object;

          assume x in ( SupBelow (R,C));

          then x = ( sup ( SetBelow (R,C,x))) by Def10;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL35:22

    

     Th22: for L be non empty reflexive transitive RelStr, R be auxiliary(i) auxiliary(ii) Relation of L, C be strict_chain of R st (for c be 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, R be auxiliary(i) auxiliary(ii) Relation of L, C be strict_chain of R;

      assume

       A1: for c be Element of L holds ex_sup_of (( SetBelow (R,C,c)),L);

      thus ( SupBelow (R,C)) is strict_chain of R

      proof

        let a,b be set;

        assume

         A2: a in ( SupBelow (R,C));

        then

         A3: a = ( sup ( SetBelow (R,C,a))) by Def10;

        reconsider 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));

        then

         A7: b = ( sup ( SetBelow (R,C,b))) by Def10;

        reconsider b as Element of L by A6;

        

         A8: b <= b;

        

         A9: ex_sup_of (( SetBelow (R,C,b)),L) by A1;

        per cases ;

          suppose a = b;

          hence thesis;

        end;

          suppose

           A10: a <> b;

          (for x be 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 be Element of L st x in C holds [x, a] in R iff [x, b] in R;

            ( SetBelow (R,C,a)) = ( SetBelow (R,C,b))

            proof

              thus ( SetBelow (R,C,a)) c= ( SetBelow (R,C,b))

              proof

                let x be object;

                assume

                 A12: x in ( SetBelow (R,C,a));

                then

                reconsider 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 thesis by A13, Th15;

              end;

              let x be object;

              assume

               A14: x in ( SetBelow (R,C,b));

              then

              reconsider 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 thesis by A15, Th15;

            end;

            hence thesis by A2, A7, Def10;

          end;

          then

          consider x be 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 thesis

          proof

            per cases by A17;

              suppose that

               A19: [x, a] in R and

               A20: not [x, b] in R;

              ( SetBelow (R,C,b)) is_<=_than x

              proof

                let y be Element of L;

                assume

                 A21: y in ( SetBelow (R,C,b));

                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;

              end;

              then b <= x by A7, A9, YELLOW_0:def 9;

              hence thesis by A4, A19, WAYBEL_4:def 4;

            end;

              suppose that

               A23: not [x, a] in R and

               A24: [x, b] in R;

              ( SetBelow (R,C,a)) is_<=_than x

              proof

                let y be Element of L;

                assume

                 A25: y in ( SetBelow (R,C,a));

                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;

              end;

              then a <= x by A3, A5, YELLOW_0:def 9;

              hence thesis by A8, A24, WAYBEL_4:def 4;

            end;

          end;

        end;

      end;

    end;

    theorem :: WAYBEL35:23

    for L be non empty Poset, R be auxiliary(i) auxiliary(ii) Relation of L, C be Subset of L st (for c be 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, R be auxiliary(i) auxiliary(ii) Relation of L, C be Subset of L;

      assume

       A1: for c be Element of L holds ex_sup_of (( SetBelow (R,C,c)),L);

      let X be Subset of ( SupBelow (R,C));

      set s = ( "\/" (X,L));

      assume

       A2: ex_sup_of (X,L);

      

       A3: ex_sup_of (( SetBelow (R,C,s)),L) by A1;

      X is_<=_than ( sup ( SetBelow (R,C,s)))

      proof

        let x be Element of L;

        

         A4: ex_sup_of (( SetBelow (R,C,x)),L) by A1;

        assume

         A5: x in X;

        then

         A6: x = ( sup ( SetBelow (R,C,x))) by Def10;

        ( SetBelow (R,C,x)) c= ( SetBelow (R,C,s)) by A2, A5, Th17, YELLOW_4: 1;

        hence x <= ( sup ( SetBelow (R,C,s))) by A3, A6, A4, YELLOW_0: 34;

      end;

      then

       A7: s <= ( sup ( SetBelow (R,C,s))) 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,s)) is_<=_than s by Th16;

      then ( sup ( SetBelow (R,C,s))) <= s by A3, YELLOW_0:def 9;

      then s = ( sup ( SetBelow (R,C,s))) by A7, ORDERS_2: 2;

      then s in ( SupBelow (R,C)) by Def10;

      hence thesis by A8, A2, YELLOW_0: 64;

    end;

    theorem :: WAYBEL35:24

    

     Th24: for L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, d be Element of L st d in ( SupBelow (R,C)) holds d = ( "\/" ({ b where b be Element of L : b in ( SupBelow (R,C)) & [b, d] in R },L))

    proof

      let L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, d be Element of L;

      deffunc F( Element of L) = { b where b be Element of L : b in ( SupBelow (R,C)) & [b, $1] in R };

      set p = ( "\/" ( F(d),L));

      

       A1: ex_sup_of (( SetBelow (R,C,d)),L) by YELLOW_0: 17;

      

       A2: F(d) is_<=_than d

      proof

        let a be Element of L;

        assume a in F(d);

        then ex b be Element of L st a = b & b in ( SupBelow (R,C)) & [b, d] in R;

        hence a <= d by WAYBEL_4:def 3;

      end;

      assume d in ( SupBelow (R,C));

      then

       A3: d = ( sup ( SetBelow (R,C,d))) by Def10;

      assume

       A4: p <> d;

       ex_sup_of ( F(d),L) by YELLOW_0: 17;

      then p <= d by A2, YELLOW_0:def 9;

      then

       A5: p < d by A4, ORDERS_2:def 6;

      now

        per cases by A3, A1, A4, YELLOW_0:def 9;

          suppose not ( SetBelow (R,C,d)) is_<=_than p;

          then

          consider a be Element of L such that

           A6: a in ( SetBelow (R,C,d)) and

           A7: not a <= p;

          

           A8: [a, d] in R by A6, Th15;

          a in C by A6, Th15;

          hence ex a be Element of L st a in C & [a, d] in R & not a <= p by A8, A7;

        end;

          suppose ex a be Element of L st ( SetBelow (R,C,d)) is_<=_than a & not p <= a;

          then

          consider a be Element of L such that

           A9: ( SetBelow (R,C,d)) is_<=_than a and

           A10: not p <= a;

          d <= a by A3, A1, A9, YELLOW_0:def 9;

          then p < a by A5, ORDERS_2: 7;

          hence ex a be Element of L st a in C & [a, d] in R & not a <= p by A10, ORDERS_2:def 6;

        end;

      end;

      then

      consider cc be Element of L such that

       A11: cc in C and

       A12: [cc, d] in R and

       A13: not cc <= p;

      per cases ;

        suppose [cc, cc] in R;

        then cc = ( sup ( SetBelow (R,C,cc))) by A11, Th18, YELLOW_0: 17;

        then cc in ( SupBelow (R,C)) by Def10;

        then cc in F(d) by A12;

        hence contradiction by A13, YELLOW_0: 17, YELLOW_4: 1;

      end;

        suppose

         A14: not [cc, cc] in R;

        ex cs be Element of L st cs in C & cc < cs & [cs, d] in R

        proof

          per cases by A3, A1, A12, A14, YELLOW_0:def 9;

            suppose not ( SetBelow (R,C,d)) is_<=_than cc;

            then

            consider cs be Element of L such that

             A15: cs in ( SetBelow (R,C,d)) and

             A16: not cs <= cc;

            take cs;

            

             A17: not [cs, cc] in R by A16, WAYBEL_4:def 3;

            thus cs in C by A15, Th15;

            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;

            thus thesis by A15, Th15;

          end;

            suppose

             A18: ex a be Element of L st ( SetBelow (R,C,d)) is_<=_than a & not cc <= a;

            cc in ( SetBelow (R,C,d)) by A11, A12, Th15;

            hence thesis by A18;

          end;

        end;

        then

        consider cs be Element of L such that

         A19: cs in C and

         A20: cc < cs and

         A21: [cs, d] in R;

        consider y be 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 F(d) by A25;

        then y <= p by YELLOW_0: 17, YELLOW_4: 1;

        then cc < p by A22, ORDERS_2: 7;

        hence contradiction by A13, ORDERS_2:def 6;

      end;

    end;

    theorem :: WAYBEL35:25

    for L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R holds R satisfies_SIC_on ( SupBelow (R,C))

    proof

      let L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R;

      let c,d be Element of L;

      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;

      

       A5: c <= d by A3, WAYBEL_4:def 3;

      deffunc F( Element of L) = { b where b be Element of L : b in ( SupBelow (R,C)) & [b, $1] in R };

      

       A6: d = ( "\/" ( F(d),L)) by A2, Th24;

      

       A7: ex_sup_of ( F(d),L) by YELLOW_0: 17;

      per cases by A4, A6, A7, YELLOW_0:def 9;

        suppose not F(d) is_<=_than c;

        then

        consider g be Element of L such that

         A8: g in F(d) and

         A9: not g <= c;

        consider y be 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 as Element of L;

        take y;

        thus y in ( SupBelow (R,C)) by A11;

        for c be 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;

        thus [y, d] in R by A12;

        thus thesis by A9, A10;

      end;

        suppose ex g be Element of L st F(d) is_<=_than g & not c <= g;

        then

        consider g be Element of L such that

         A13: F(d) is_<=_than g and

         A14: not c <= g;

        d <= g by A6, A7, A13, YELLOW_0:def 9;

        hence thesis by A5, A14, ORDERS_2: 3;

      end;

    end;

    theorem :: WAYBEL35:26

    for L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, a,b be Element of L st a in C & b in C & a < b holds ex d be Element of L st d in ( SupBelow (R,C)) & a < d & [d, b] in R

    proof

      let L be complete non empty Poset, R be extra-order Relation of L, C be satisfying_SIC strict_chain of R, a,b be Element of L;

      assume that

       A1: a in C and

       A2: b in C and

       A3: a < b;

      consider d be 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;

      thus thesis by A4, A5, A6, Def10;

    end;