yellow_1.miz

    begin

    reserve X for set;

    registration

      let L be Lattice;

      cluster ( LattPOSet L) -> with_suprema with_infima;

      coherence by LATTICE3: 11;

    end

    registration

      let L be upper-bounded Lattice;

      cluster ( LattPOSet L) -> upper-bounded;

      coherence

      proof

        ex x be Element of ( LattPOSet L) st x is_>=_than the carrier of ( LattPOSet L)

        proof

          take x = ( Top ( LattPOSet L));

          consider z be Element of L such that

           A1: for v be Element of L holds (z "\/" v) = z & (v "\/" z) = z by LATTICES:def 14;

          reconsider z9 = z as Element of ( LattPOSet L);



           A2: z = ( Top L) by A1, LATTICES:def 17;

           A3:

          now

            let b9 be Element of ( LattPOSet L);

            reconsider b = b9 as Element of L;

            assume b9 is_<=_than {} ;



             A4: (b % ) = b & (z % ) = z;

            b [= z by A2, LATTICES: 19;

            hence z9 >= b9 by A4, LATTICE3: 7;

          end;

          z9 is_<=_than {} ;

          then

           A5: z9 = ( "/\" ( {} ,( LattPOSet L))) by A3, YELLOW_0: 31;

          now

            reconsider x9 = x as Element of L;

            let a be Element of ( LattPOSet L);

            assume a in the carrier of ( LattPOSet L);

            reconsider a9 = a as Element of L;

            ( Top ( LattPOSet L)) = ( Top L) by A2, A5, YELLOW_0:def 12;

            then

             A6: a9 [= x9 by LATTICES: 19;

            (a9 % ) = a9 & (x9 % ) = x9;

            hence a <= x by A6, LATTICE3: 7;

          end;

          hence thesis;

        end;

        hence thesis by YELLOW_0:def 5;

      end;

    end

    registration

      let L be lower-bounded Lattice;

      cluster ( LattPOSet L) -> lower-bounded;

      coherence

      proof

        ex x be Element of ( LattPOSet L) st x is_<=_than the carrier of ( LattPOSet L)

        proof

          take x = ( Bottom ( LattPOSet L));

          consider z be Element of L such that

           A1: for v be Element of L holds (z "/\" v) = z & (v "/\" z) = z by LATTICES:def 13;

          reconsider z9 = z as Element of ( LattPOSet L);



           A2: z = ( Bottom L) by A1, LATTICES:def 16;

           A3:

          now

            let b9 be Element of ( LattPOSet L);

            reconsider b = b9 as Element of L;

            assume b9 is_>=_than {} ;



             A4: (b % ) = b & (z % ) = z;

            z [= b by A2, LATTICES: 16;

            hence z9 <= b9 by A4, LATTICE3: 7;

          end;

          z9 is_>=_than {} ;

          then

           A5: z9 = ( "\/" ( {} ,( LattPOSet L))) by A3, YELLOW_0: 30;

          now

            reconsider x9 = x as Element of L;

            let a be Element of ( LattPOSet L);

            assume a in the carrier of ( LattPOSet L);

            reconsider a9 = a as Element of L;

            ( Bottom ( LattPOSet L)) = ( Bottom L) by A2, A5, YELLOW_0:def 11;

            then

             A6: x9 [= a9 by LATTICES: 16;

            (a9 % ) = a9 & (x9 % ) = x9;

            hence x <= a by A6, LATTICE3: 7;

          end;

          hence thesis;

        end;

        hence thesis by YELLOW_0:def 4;

      end;

    end

    registration

      let L be complete Lattice;

      cluster ( LattPOSet L) -> complete;

      coherence

      proof

        for X be set holds ex a be Element of ( LattPOSet L) st X is_<=_than a & for b be Element of ( LattPOSet L) st X is_<=_than b holds a <= b

        proof

          let X be set;

          take a = ( "\/" (X,( LattPOSet L)));

          X is_less_than ( "\/" (X,L)) by LATTICE3:def 21;

          then X is_<=_than (( "\/" (X,L)) % ) by LATTICE3: 30;

          hence X is_<=_than a by YELLOW_0: 29;

          let b be Element of ( LattPOSet L);

          reconsider b9 = b as Element of L;

          assume X is_<=_than b;

          then X is_<=_than (b9 % );

          then X is_less_than b9 by LATTICE3: 30;

          then

           A1: ( "\/" (X,L)) [= b9 by LATTICE3:def 21;

          (( "\/" (X,L)) % ) = a & (b9 % ) = b by YELLOW_0: 29;

          hence thesis by A1, LATTICE3: 7;

        end;

        hence thesis;

      end;

    end

    definition

      let X be set;

      :: YELLOW_1:def1

      func InclPoset X -> strict RelStr equals RelStr (# X, ( RelIncl X) #);

      correctness ;

    end

    registration

      let X be set;

      cluster ( InclPoset X) -> reflexive antisymmetric transitive;

      coherence ;

    end

    registration

      let X be non empty set;

      cluster ( InclPoset X) -> non empty;

      coherence ;

    end

    theorem :: YELLOW_1:1

    the carrier of ( InclPoset X) = X & the InternalRel of ( InclPoset X) = ( RelIncl X);

    definition

      let X be set;

      :: YELLOW_1:def2

      func BoolePoset X -> strict RelStr equals ( LattPOSet ( BooleLatt X));

      correctness ;

    end

    registration

      let X be set;

      cluster ( BoolePoset X) -> non empty reflexive antisymmetric transitive;

      coherence ;

    end

    registration

      let X be set;

      cluster ( BoolePoset X) -> complete;

      coherence ;

    end

    theorem :: YELLOW_1:2



     Th2: for x,y be Element of ( BoolePoset X) holds x <= y iff x c= y

    proof

      let x,y be Element of ( BoolePoset X);

      reconsider x9 = x, y9 = y as Element of ( BooleLatt X);

      thus x <= y implies x c= y

      proof

        assume x <= y;

        then (x9 % ) <= (y9 % );

        then x9 [= y9 by LATTICE3: 7;

        hence thesis by LATTICE3: 2;

      end;

      assume x c= y;

      then x9 [= y9 by LATTICE3: 2;

      then (x9 % ) <= (y9 % ) by LATTICE3: 7;

      hence thesis;

    end;

    theorem :: YELLOW_1:3



     Th3: for X be non empty set, x,y be Element of ( InclPoset X) holds x <= y iff x c= y

    proof

      let X be non empty set;

      let x,y be Element of ( InclPoset X);

      thus x <= y implies x c= y

      proof

        assume x <= y;

        then [x, y] in the InternalRel of ( InclPoset X) by ORDERS_2:def 5;

        hence thesis by WELLORD2:def 1;

      end;

      thus x c= y implies x <= y

      proof

        assume x c= y;

        then [x, y] in ( RelIncl X) by WELLORD2:def 1;

        hence thesis by ORDERS_2:def 5;

      end;

    end;

    theorem :: YELLOW_1:4



     Th4: ( BoolePoset X) = ( InclPoset ( bool X))

    proof

      set B = ( BoolePoset X);

      the carrier of B = ( bool X) by LATTICE3:def 1;

      then

      reconsider In = the InternalRel of B as Relation of ( bool X);

      for x be object st x in ( bool X) holds ex y be object st [x, y] in In

      proof

        let x be object;

        assume x in ( bool X);

        then

        reconsider x9 = x as Element of B by LATTICE3:def 1;

        take y = x9;

        x9 <= y;

        hence thesis by ORDERS_2:def 5;

      end;

      then

       A1: ( dom In) = ( bool X) by RELSET_1: 9;

       A2:

      now

        let Y,Z be set;

        assume Y in ( bool X) & Z in ( bool X);

        then

        reconsider Y9 = Y, Z9 = Z as Element of B by LATTICE3:def 1;

        thus [Y, Z] in the InternalRel of B implies Y c= Z

        proof

          assume [Y, Z] in the InternalRel of B;

          then Y9 <= Z9 by ORDERS_2:def 5;

          hence thesis by Th2;

        end;

        thus Y c= Z implies [Y, Z] in the InternalRel of B

        proof

          assume Y c= Z;

          then Y9 <= Z9 by Th2;

          hence thesis by ORDERS_2:def 5;

        end;

      end;

      for y be object st y in ( bool X) holds ex x be object st [x, y] in In

      proof

        let y be object;

        assume y in ( bool X);

        then

        reconsider y9 = y as Element of B by LATTICE3:def 1;

        take x = y9;

        x <= y9;

        hence thesis by ORDERS_2:def 5;

      end;

      then ( field the InternalRel of B) = (( bool X) \/ ( bool X)) by A1, RELSET_1: 10;

      then the InternalRel of B = ( RelIncl ( bool X)) by A2, WELLORD2:def 1;

      hence thesis by LATTICE3:def 1;

    end;

    theorem :: YELLOW_1:5

    for Y be Subset-Family of X holds ( InclPoset Y) is full SubRelStr of ( BoolePoset X)

    proof

      set L = ( BoolePoset X);

      let Y be Subset-Family of X;

      reconsider Y9 = Y as Subset of L by LATTICE3:def 1;

      the carrier of L = ( bool X) by LATTICE3:def 1;

      then

      reconsider In = the InternalRel of L as Relation of ( bool X);

      for x be object st x in ( bool X) holds ex y be object st [x, y] in In

      proof

        let x be object;

        assume x in ( bool X);

        then

        reconsider x9 = x as Element of L by LATTICE3:def 1;

        take y = x9;

        x9 <= y;

        hence thesis by ORDERS_2:def 5;

      end;

      then

       A1: ( dom In) = ( bool X) by RELSET_1: 9;

       A2:

      now

        let Y,Z be set;

        assume Y in ( bool X) & Z in ( bool X);

        then

        reconsider Y9 = Y, Z9 = Z as Element of L by LATTICE3:def 1;

        thus [Y, Z] in the InternalRel of L implies Y c= Z

        proof

          assume [Y, Z] in the InternalRel of L;

          then Y9 <= Z9 by ORDERS_2:def 5;

          hence thesis by Th2;

        end;

        thus Y c= Z implies [Y, Z] in the InternalRel of L

        proof

          assume Y c= Z;

          then Y9 <= Z9 by Th2;

          hence thesis by ORDERS_2:def 5;

        end;

      end;

      for y be object st y in ( bool X) holds ex x be object st [x, y] in In

      proof

        let y be object;

        assume y in ( bool X);

        then

        reconsider y9 = y as Element of L by LATTICE3:def 1;

        take x = y9;

        x <= y9;

        hence thesis by ORDERS_2:def 5;

      end;

      then ( field the InternalRel of L) = (( bool X) \/ ( bool X)) by A1, RELSET_1: 10;

      then

       A3: the InternalRel of L = ( RelIncl ( bool X)) by A2, WELLORD2:def 1;

       RelStr (# Y9, (the InternalRel of L |_2 Y9) #) is full SubRelStr of L by YELLOW_0: 56;

      hence thesis by A3, WELLORD2: 7;

    end;

    theorem :: YELLOW_1:6

    for X be non empty set holds ( InclPoset X) is with_suprema implies for x,y be Element of ( InclPoset X) holds (x \/ y) c= (x "\/" y)

    proof

      let X be non empty set;

      assume

       A1: ( InclPoset X) is with_suprema;

      let x,y be Element of ( InclPoset X);

      y <= (x "\/" y) by A1, YELLOW_0: 22;

      then

       A2: y c= (x "\/" y) by Th3;

      x <= (x "\/" y) by A1, YELLOW_0: 22;

      then x c= (x "\/" y) by Th3;

      hence thesis by A2, XBOOLE_1: 8;

    end;

    theorem :: YELLOW_1:7

    for X be non empty set holds ( InclPoset X) is with_infima implies for x,y be Element of ( InclPoset X) holds (x "/\" y) c= (x /\ y)

    proof

      let X be non empty set;

      assume

       A1: ( InclPoset X) is with_infima;

      let x,y be Element of ( InclPoset X);

      (x "/\" y) <= y by A1, YELLOW_0: 23;

      then

       A2: (x "/\" y) c= y by Th3;

      (x "/\" y) <= x by A1, YELLOW_0: 23;

      then (x "/\" y) c= x by Th3;

      hence thesis by A2, XBOOLE_1: 19;

    end;

    theorem :: YELLOW_1:8



     Th8: for X be non empty set holds for x,y be Element of ( InclPoset X) st (x \/ y) in X holds (x "\/" y) = (x \/ y)

    proof

      let X be non empty set;

      let x,y be Element of ( InclPoset X);

      assume (x \/ y) in X;

      then

      reconsider z = (x \/ y) as Element of ( InclPoset X);

      y c= z by XBOOLE_1: 7;

      then

       A1: y <= z by Th3;

       A2:

      now

        let c be Element of ( InclPoset X);

        assume x <= c & y <= c;

        then x c= c & y c= c by Th3;

        then z c= c by XBOOLE_1: 8;

        hence z <= c by Th3;

      end;

      x c= z by XBOOLE_1: 7;

      then x <= z by Th3;

      hence thesis by A1, A2, LATTICE3:def 13;

    end;

    theorem :: YELLOW_1:9



     Th9: for X be non empty set holds for x,y be Element of ( InclPoset X) st (x /\ y) in X holds (x "/\" y) = (x /\ y)

    proof

      let X be non empty set;

      let x,y be Element of ( InclPoset X);

      assume (x /\ y) in X;

      then

      reconsider z = (x /\ y) as Element of ( InclPoset X);

      z c= y by XBOOLE_1: 17;

      then

       A1: z <= y by Th3;

       A2:

      now

        let c be Element of ( InclPoset X);

        assume c <= x & c <= y;

        then c c= x & c c= y by Th3;

        then c c= z by XBOOLE_1: 19;

        hence c <= z by Th3;

      end;

      z c= x by XBOOLE_1: 17;

      then z <= x by Th3;

      hence thesis by A1, A2, LATTICE3:def 14;

    end;

    theorem :: YELLOW_1:10

    for L be RelStr st for x,y be Element of L holds x <= y iff x c= y holds the InternalRel of L = ( RelIncl the carrier of L)

    proof

      let L be RelStr;

      assume

       A1: for x,y be Element of L holds x <= y iff x c= y;

       A2:

      now

        let Y,Z be set;

        assume Y in the carrier of L & Z in the carrier of L;

        then

        reconsider Y9 = Y, Z9 = Z as Element of L;

        thus [Y, Z] in the InternalRel of L implies Y c= Z

        proof

          assume [Y, Z] in the InternalRel of L;

          then Y9 <= Z9 by ORDERS_2:def 5;

          hence thesis by A1;

        end;

        thus Y c= Z implies [Y, Z] in the InternalRel of L

        proof

          assume Y c= Z;

          then Y9 <= Z9 by A1;

          hence thesis by ORDERS_2:def 5;

        end;

      end;

      for x be object st x in the carrier of L holds ex y be object st [x, y] in the InternalRel of L

      proof

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x9 = x as Element of L;

        take y = x9;

        x9 <= y by A1;

        hence thesis by ORDERS_2:def 5;

      end;

      then

       A3: ( dom the InternalRel of L) = the carrier of L by RELSET_1: 9;

      for y be object st y in the carrier of L holds ex x be object st [x, y] in the InternalRel of L

      proof

        let y be object;

        assume y in the carrier of L;

        then

        reconsider y9 = y as Element of L;

        take x = y9;

        x <= y9 by A1;

        hence thesis by ORDERS_2:def 5;

      end;

      then ( field the InternalRel of L) = (the carrier of L \/ the carrier of L) by A3, RELSET_1: 10;

      hence thesis by A2, WELLORD2:def 1;

    end;

    theorem :: YELLOW_1:11

    for X be non empty set st (for x,y be set st (x in X & y in X) holds (x \/ y) in X) holds ( InclPoset X) is with_suprema

    proof

      let X be non empty set;

      set L = ( InclPoset X);

      assume

       A1: for x,y be set st x in X & y in X holds (x \/ y) in X;

      now

        let a,b be Element of L;

        ex c be Element of L st {a, b} is_<=_than c & for d be Element of L st {a, b} is_<=_than d holds c <= d

        proof

          take c = (a "\/" b);



           A2: (a \/ b) = c by A1, Th8;

          then b c= c by XBOOLE_1: 7;

          then

           A3: b <= c by Th3;

          a c= c by A2, XBOOLE_1: 7;

          then a <= c by Th3;

          hence {a, b} is_<=_than c by A3, YELLOW_0: 8;

          let d be Element of L;

          assume

           A4: {a, b} is_<=_than d;

          b in {a, b} by TARSKI:def 2;

          then b <= d by A4;

          then

           A5: b c= d by Th3;

          a in {a, b} by TARSKI:def 2;

          then a <= d by A4;

          then a c= d by Th3;

          then (a \/ b) c= d by A5, XBOOLE_1: 8;

          then c c= d by A1, Th8;

          hence thesis by Th3;

        end;

        hence ex_sup_of ( {a, b},L) by YELLOW_0: 15;

      end;

      hence thesis by YELLOW_0: 20;

    end;

    theorem :: YELLOW_1:12

    for X be non empty set st for x,y be set st x in X & y in X holds (x /\ y) in X holds ( InclPoset X) is with_infima

    proof

      let X be non empty set;

      set L = ( InclPoset X);

      assume

       A1: for x,y be set st x in X & y in X holds (x /\ y) in X;

      now

        let a,b be Element of L;

        ex c be Element of L st {a, b} is_>=_than c & for d be Element of L st {a, b} is_>=_than d holds c >= d

        proof

          take c = (a "/\" b);



           A2: (a /\ b) = c by A1, Th9;

          then c c= b by XBOOLE_1: 17;

          then

           A3: c <= b by Th3;

          c c= a by A2, XBOOLE_1: 17;

          then c <= a by Th3;

          hence {a, b} is_>=_than c by A3, YELLOW_0: 8;

          let d be Element of L;

          assume

           A4: {a, b} is_>=_than d;

          b in {a, b} by TARSKI:def 2;

          then d <= b by A4;

          then

           A5: d c= b by Th3;

          a in {a, b} by TARSKI:def 2;

          then d <= a by A4;

          then d c= a by Th3;

          then d c= (a /\ b) by A5, XBOOLE_1: 19;

          then d c= c by A1, Th9;

          hence thesis by Th3;

        end;

        hence ex_inf_of ( {a, b},L) by YELLOW_0: 16;

      end;

      hence thesis by YELLOW_0: 21;

    end;

    theorem :: YELLOW_1:13



     Th13: for X be non empty set holds {} in X implies ( Bottom ( InclPoset X)) = {}

    proof

      let X be non empty set;

      assume {} in X;

      then

      reconsider a = {} as Element of ( InclPoset X);

      for b be Element of ( InclPoset X) st b in X holds a <= b by Th3, XBOOLE_1: 2;

      then a is_<=_than X;

      then ( InclPoset X) is lower-bounded by YELLOW_0:def 4;

      then {} is_<=_than a & ex_sup_of ( {} ,( InclPoset X)) by YELLOW_0: 42;

      then ( "\/" ( {} ,( InclPoset X))) <= a by YELLOW_0:def 9;

      then

       A1: ( "\/" ( {} ,( InclPoset X))) c= a by Th3;



      thus ( Bottom ( InclPoset X)) = ( "\/" ( {} ,( InclPoset X))) by YELLOW_0:def 11

      .= {} by A1;

    end;

    theorem :: YELLOW_1:14



     Th14: for X be non empty set holds ( union X) in X implies ( Top ( InclPoset X)) = ( union X)

    proof

      let X be non empty set;

      assume ( union X) in X;

      then

      reconsider a = ( union X) as Element of ( InclPoset X);

      for b be Element of ( InclPoset X) st b in X holds b <= a by Th3, ZFMISC_1: 74;

      then a is_>=_than X;

      then ( InclPoset X) is upper-bounded by YELLOW_0:def 5;

      then {} is_>=_than a & ex_inf_of ( {} ,( InclPoset X)) by YELLOW_0: 43;

      then a <= ( "/\" ( {} ,( InclPoset X))) by YELLOW_0:def 10;

      then

       A1: ( "/\" ( {} ,( InclPoset X))) c= a & a c= ( "/\" ( {} ,( InclPoset X))) by Th3, ZFMISC_1: 74;



      thus ( Top ( InclPoset X)) = ( "/\" ( {} ,( InclPoset X))) by YELLOW_0:def 12

      .= ( union X) by A1;

    end;

    theorem :: YELLOW_1:15

    for X be non empty set holds ( InclPoset X) is upper-bounded implies ( union X) in X

    proof

      let X be non empty set;

      assume ( InclPoset X) is upper-bounded;

      then

      consider x be Element of ( InclPoset X) such that

       A1: x is_>=_than the carrier of ( InclPoset X) by YELLOW_0:def 5;

      now

        let y be object;

        assume y in ( union X);

        then

        consider Y be set such that

         A2: y in Y and

         A3: Y in X by TARSKI:def 4;

        reconsider Y as Element of ( InclPoset X) by A3;

        Y <= x by A1;

        then Y c= x by Th3;

        hence y in x by A2;

      end;

      then

       A4: ( union X) c= x;

      x in X & x c= ( union X) by ZFMISC_1: 74;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: YELLOW_1:16

    for X be non empty set holds ( InclPoset X) is lower-bounded implies ( meet X) in X

    proof

      let X be non empty set;

      assume ( InclPoset X) is lower-bounded;

      then

      consider x be Element of ( InclPoset X) such that

       A1: x is_<=_than the carrier of ( InclPoset X) by YELLOW_0:def 4;

      now

        let y be object;

        assume

         A2: y in x;

        now

          let Y be set;

          assume Y in X;

          then

          reconsider Y9 = Y as Element of ( InclPoset X);

          x <= Y9 by A1;

          then x c= Y9 by Th3;

          hence y in Y by A2;

        end;

        hence y in ( meet X) by SETFAM_1:def 1;

      end;

      then

       A3: x c= ( meet X);

      x in X & ( meet X) c= x by SETFAM_1: 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;



     Lm1: for x,y be Element of ( BoolePoset X) holds (x /\ y) in ( bool X) & (x \/ y) in ( bool X)

    proof

      let x,y be Element of ( BoolePoset X);

      x in the carrier of ( BoolePoset X);

      then

       A1: x in ( bool X) by LATTICE3:def 1;

      then (x /\ y) c= X by XBOOLE_1: 108;

      hence (x /\ y) in ( bool X);

      y in the carrier of ( BoolePoset X);

      then y in ( bool X) by LATTICE3:def 1;

      then (x \/ y) c= X by A1, XBOOLE_1: 8;

      hence thesis;

    end;

    theorem :: YELLOW_1:17

    for x,y be Element of ( BoolePoset X) holds (x "\/" y) = (x \/ y) & (x "/\" y) = (x /\ y)

    proof

      let x,y be Element of ( BoolePoset X);

      reconsider x, y as Element of ( InclPoset ( bool X)) by Th4;

      (x "/\" y) = (x /\ y) & (x "\/" y) = (x \/ y) by Lm1, Th8, Th9;

      hence thesis by Th4;

    end;

    theorem :: YELLOW_1:18

    ( Bottom ( BoolePoset X)) = {}

    proof



      thus ( Bottom ( BoolePoset X)) = ( "\/" ( {} ,( LattPOSet ( BooleLatt X)))) by YELLOW_0:def 11

      .= ( "\/" ( {} ,( BooleLatt X))) by YELLOW_0: 29

      .= ( Bottom ( BooleLatt X)) by LATTICE3: 49

      .= {} by LATTICE3: 3;

    end;

    theorem :: YELLOW_1:19

    ( Top ( BoolePoset X)) = X

    proof



       A1: ( Top ( InclPoset ( bool X))) = ( union ( bool X)) by Th14;

      ( BoolePoset X) = ( InclPoset ( bool X)) by Th4;

      hence thesis by A1, ZFMISC_1: 81;

    end;

    theorem :: YELLOW_1:20

    for Y be non empty Subset of ( BoolePoset X) holds ( inf Y) = ( meet Y)

    proof

      set L = ( BoolePoset X);

      let Y be non empty Subset of L;

      set y = the Element of Y;



       A1: the carrier of L = ( bool X) by LATTICE3:def 1;

      then y c= X;

      then

      reconsider Me = ( meet Y) as Element of L by A1, SETFAM_1: 7;

       A2:

      now

        let b be Element of L;

        assume

         A3: b is_<=_than Y;

        for Z be set st Z in Y holds b c= Z by Th2, A3;

        then b c= Me by SETFAM_1: 5;

        hence Me >= b by Th2;

      end;

      for b be Element of L st b in Y holds Me <= b by Th2, SETFAM_1: 3;

      then Me is_<=_than Y;

      hence thesis by A2, YELLOW_0: 33;

    end;

    theorem :: YELLOW_1:21

    for Y be Subset of ( BoolePoset X) holds ( sup Y) = ( union Y)

    proof

      set L = ( BoolePoset X);

      let Y be Subset of L;



       A1: the carrier of L = ( bool X) by LATTICE3:def 1;

      then ( union Y) c= ( union ( bool X)) by ZFMISC_1: 77;

      then

      reconsider Un = ( union Y) as Element of L by A1, ZFMISC_1: 81;

       A2:

      now

        let b be Element of L;

        assume

         A3: b is_>=_than Y;

        for Z be set st Z in Y holds Z c= b by Th2, A3;

        then Un c= b by ZFMISC_1: 76;

        hence Un <= b by Th2;

      end;

      for b be Element of L st b in Y holds b <= Un by Th2, ZFMISC_1: 74;

      then Un is_>=_than Y;

      hence thesis by A2, YELLOW_0: 30;

    end;

    theorem :: YELLOW_1:22

    for T be non empty TopSpace, X be Subset of ( InclPoset the topology of T) holds ( sup X) = ( union X)

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      let X be Subset of L;

      reconsider X as Subset-Family of T by XBOOLE_1: 1;

      reconsider Un = ( union X) as Element of L by PRE_TOPC:def 1;

       A1:

      now

        let b be Element of L;

        assume b is_>=_than X;

        then for Z be set st Z in X holds Z c= b by Th3;

        then Un c= b by ZFMISC_1: 76;

        hence Un <= b by Th3;

      end;

      for b be Element of L st b in X holds b <= Un by Th3, ZFMISC_1: 74;

      then Un is_>=_than X;

      hence thesis by A1, YELLOW_0: 30;

    end;

    theorem :: YELLOW_1:23

    for T be non empty TopSpace holds ( Bottom ( InclPoset the topology of T)) = {} by Th13, PRE_TOPC: 1;



     Lm2: for T be non empty TopSpace holds ( InclPoset the topology of T) is lower-bounded

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      reconsider x = {} as Element of L by PRE_TOPC: 1;

      now

        take x;

        thus x is_<=_than the carrier of L

        proof

          let b be Element of L;

          assume b in the carrier of L;

          x c= b;

          hence thesis by Th3;

        end;

      end;

      hence thesis by YELLOW_0:def 4;

    end;

    theorem :: YELLOW_1:24

    for T be non empty TopSpace holds ( Top ( InclPoset the topology of T)) = the carrier of T

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T), C = the carrier of T;

      the carrier of T = ( "/\" ( {} ,L))

      proof

        reconsider C as Element of L by PRE_TOPC:def 1;



         A1: for b be Element of L st b is_<=_than {} holds C >= b

        proof

          let b be Element of L;

          assume b is_<=_than {} ;

          b in the topology of T;

          hence thesis by Th3;

        end;

        C is_<=_than {} ;

        hence thesis by A1, YELLOW_0: 31;

      end;

      hence thesis by YELLOW_0:def 12;

    end;



     Lm3: for T be non empty TopSpace holds ( InclPoset the topology of T) is complete

    proof

      let T be non empty TopSpace;

      set A = the topology of T;

      reconsider IA = ( InclPoset A) as lower-bounded Poset by Lm2;

      for X be Subset of IA holds ex_sup_of (X,( InclPoset A))

      proof

        let X be Subset of IA;

        set N = ( union X);

        reconsider X9 = X as Subset-Family of T by XBOOLE_1: 1;

        X9 c= the topology of T;

        then

        reconsider N as Element of ( InclPoset A) by PRE_TOPC:def 1;



         A1: for b be Element of ( InclPoset A) st X is_<=_than b holds N <= b

        proof

          let b be Element of ( InclPoset A);

          assume X is_<=_than b;

          then for Z1 be set st Z1 in X holds Z1 c= b by Th3;

          then ( union X) c= b by ZFMISC_1: 76;

          hence thesis by Th3;

        end;

        X is_<=_than N by ZFMISC_1: 74, Th3;

        hence thesis by A1, YELLOW_0: 15;

      end;

      hence thesis by YELLOW_0: 53;

    end;



     Lm4: for T be non empty TopSpace holds ( InclPoset the topology of T) is non trivial

    proof

      let T be non empty TopSpace;

      set L = ( InclPoset the topology of T);

      reconsider E = {} , S = the carrier of T as Element of L by PRE_TOPC: 1, PRE_TOPC:def 1;

      E <> S;

      hence thesis by STRUCT_0:def 10;

    end;

    registration

      let T be non empty TopSpace;

      cluster ( InclPoset the topology of T) -> complete non trivial;

      coherence by Lm3, Lm4;

    end

    theorem :: YELLOW_1:25

    for T be TopSpace, F be Subset-Family of T holds F is open iff F is Subset of ( InclPoset the topology of T)

    proof

      let T be TopSpace;

      let F be Subset-Family of T;

      hereby

        assume

         A1: F is open;

        F c= the topology of T by A1, PRE_TOPC:def 2;

        hence F is Subset of ( InclPoset the topology of T);

      end;

      assume

       A2: F is Subset of ( InclPoset the topology of T);

      let P be Subset of T;

      assume P in F;

      hence thesis by A2, PRE_TOPC:def 2;

    end;

    begin

    reserve x,y,z for set;

    definition

      let R be Relation;

      :: YELLOW_1:def3

      attr R is RelStr-yielding means

      : Def3: for v be set st v in ( rng R) holds v is RelStr;

    end

    registration

      cluster RelStr-yielding -> 1-sorted-yielding for Function;

      coherence

      proof

        let F be Function such that

         A1: F is RelStr-yielding;

        let x be object;

        assume x in ( dom F);

        then (F . x) in ( rng F) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

    end

    registration

      let I be set;

      cluster RelStr-yielding for ManySortedSet of I;

      existence

      proof

        set R = the RelStr;

        take (I --> R);

        let v be set;

        assume

         A1: v in ( rng (I --> R));

        ( rng (I --> R)) c= {R} by FUNCOP_1: 13;

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    definition

      let J be non empty set, A be RelStr-yielding ManySortedSet of J, j be Element of J;

      :: original: .

      redefine

      func A . j -> RelStr ;

      coherence

      proof

        ( dom A) = J by PARTFUN1:def 2;

        then (A . j) in ( rng A) by FUNCT_1:def 3;

        hence thesis by Def3;

      end;

    end

    definition

      let I be set;

      let J be RelStr-yielding ManySortedSet of I;

      :: YELLOW_1:def4

      func product J -> strict RelStr means

      : Def4: the carrier of it = ( product ( Carrier J)) & for x,y be Element of it st x in ( product ( Carrier J)) holds x <= y iff ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi;

      existence

      proof

        defpred P[ object, object] means ex f,g be Function st f = $1 & g = $2 & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi;

        consider R be Relation of ( product ( Carrier J)) such that

         A1: for x,y be object holds [x, y] in R iff x in ( product ( Carrier J)) & y in ( product ( Carrier J)) & P[x, y] from RELSET_1:sch 1;

        take RS = RelStr (# ( product ( Carrier J)), R #);

        thus the carrier of RS = ( product ( Carrier J));

        let x,y be Element of RS such that

         A2: x in ( product ( Carrier J));

        hereby

          assume x <= y;

          then [x, y] in the InternalRel of RS by ORDERS_2:def 5;

          hence ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A1;

        end;

        assume ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi;

        then [x, y] in the InternalRel of RS by A1, A2;

        hence thesis by ORDERS_2:def 5;

      end;

      uniqueness

      proof

        let S1,S2 be strict RelStr such that

         A3: the carrier of S1 = ( product ( Carrier J)) and

         A4: for x,y be Element of S1 st x in ( product ( Carrier J)) holds x <= y iff ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi and

         A5: the carrier of S2 = ( product ( Carrier J)) and

         A6: for x,y be Element of S2 st x in ( product ( Carrier J)) holds x <= y iff ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi;

        the InternalRel of S1 = the InternalRel of S2

        proof

          let a,b be object;

          hereby

            assume

             A7: [a, b] in the InternalRel of S1;

            then

            reconsider x = a, y = b as Element of S1 by ZFMISC_1: 87;

            reconsider x9 = x, y9 = y as Element of S2 by A3, A5;



             A8: a in the carrier of S1 by A7, ZFMISC_1: 87;

            x <= y by A7, ORDERS_2:def 5;

            then ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A3, A4, A8;

            then x9 <= y9 by A3, A6, A8;

            hence [a, b] in the InternalRel of S2 by ORDERS_2:def 5;

          end;

          assume

           A9: [a, b] in the InternalRel of S2;

          then

          reconsider x = a, y = b as Element of S2 by ZFMISC_1: 87;

          reconsider x9 = x, y9 = y as Element of S1 by A3, A5;



           A10: a in the carrier of S2 by A9, ZFMISC_1: 87;

          x <= y by A9, ORDERS_2:def 5;

          then ex f,g be Function st f = x & g = y & for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A5, A6, A10;

          then x9 <= y9 by A4, A5, A10;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis by A3, A5;

      end;

    end

    registration

      let X be set;

      let L be RelStr;

      cluster (X --> L) -> RelStr-yielding;

      coherence

      proof

        let v be set;

        assume

         A1: v in ( rng (X --> L));

        ( rng (X --> L)) c= {L} by FUNCOP_1: 13;

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    definition

      let I be set;

      let T be RelStr;

      :: YELLOW_1:def5

      func T |^ I -> strict RelStr equals ( product (I --> T));

      correctness ;

    end

    theorem :: YELLOW_1:26



     Th26: for J be RelStr-yielding ManySortedSet of {} holds ( product J) = RelStr (# { {} }, ( id { {} }) #)

    proof

      let J be RelStr-yielding ManySortedSet of {} ;

      set IT = ( product J);



       A1: the carrier of IT = ( product ( Carrier J)) by Def4

      .= { {} } by CARD_3: 10, PBOOLE: 122;



       A2: ( product ( Carrier J)) = { {} } by CARD_3: 10, PBOOLE: 122;

      the InternalRel of ( product J) = ( id { {} })

      proof

        reconsider x = {} , y = {} as Element of IT by A1, TARSKI:def 1;

        let a,b be object;

        x = ( {} --> { {} });

        then

        reconsider f = x, g = y as Function;

        hereby

          assume

           A3: [a, b] in the InternalRel of IT;

          then

           A4: b in the carrier of IT by ZFMISC_1: 87;



           A5: a in the carrier of IT by A3, ZFMISC_1: 87;

          then a = {} by A1, TARSKI:def 1;

          then a = b by A1, A4, TARSKI:def 1;

          hence [a, b] in ( id { {} }) by A1, A5, RELAT_1:def 10;

        end;

        assume

         A6: [a, b] in ( id { {} });

        then a in { {} } by RELAT_1:def 10;

        then

         A7: a = {} by TARSKI:def 1;

        for i be object st i in {} holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (f . i) & yi = (g . i) & xi <= yi;

        then

         A8: x <= y by A1, A2, Def4;

        a = b by A6, RELAT_1:def 10;

        hence thesis by A7, A8, ORDERS_2:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: YELLOW_1:27

    for Y be RelStr holds (Y |^ {} ) = RelStr (# { {} }, ( id { {} }) #) by Th26;

    theorem :: YELLOW_1:28



     Th28: for X be set, Y be RelStr holds ( Funcs (X,the carrier of Y)) = the carrier of (Y |^ X)

    proof

      let X be set;

      let Y be RelStr;

      set YY = the carrier of Y, f = ( Carrier (X --> Y));



       A1: ( dom f) = X by PARTFUN1:def 2;



       A2: for x be set st x in X holds (f . x) = YY

      proof

        let x be set;

        assume

         A3: x in X;

        then ex R be 1-sorted st R = ((X --> Y) . x) & (f . x) = the carrier of R by PRALG_1:def 15;

        hence thesis by A3, FUNCOP_1: 7;

      end;

      ( Funcs (X,YY)) = ( product f)

      proof

        thus ( Funcs (X,YY)) c= ( product f)

        proof

          let x be object;

          assume x in ( Funcs (X,YY));

          then

          consider g be Function such that

           A4: x = g and

           A5: ( dom g) = X and

           A6: ( rng g) c= YY by FUNCT_2:def 2;

          now

            let y be object;

            assume y in ( dom f);

            then (f . y) = YY & (g . y) in ( rng g) by A2, A5, FUNCT_1:def 3;

            hence (g . y) in (f . y) by A6;

          end;

          hence thesis by A1, A4, A5, CARD_3:def 5;

        end;

        let x be object;

        assume x in ( product f);

        then

        consider g be Function such that

         A7: x = g and

         A8: ( dom g) = ( dom f) and

         A9: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;

        ( rng g) c= YY

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider z be object such that

           A10: z in ( dom g) and

           A11: y = (g . z) by FUNCT_1:def 3;

          (f . z) = YY by A2, A8, A10;

          hence thesis by A8, A9, A10, A11;

        end;

        hence thesis by A1, A7, A8, FUNCT_2:def 2;

      end;

      hence thesis by Def4;

    end;

    registration

      let X be set;

      let Y be non empty RelStr;

      cluster (Y |^ X) -> non empty;

      coherence

      proof

        set f = the Function of X, the carrier of Y;

        f in ( Funcs (X,the carrier of Y)) by FUNCT_2: 8;

        hence thesis by Th28;

      end;

    end



     Lm5: for X be set, Y be non empty RelStr holds for x be Element of (Y |^ X) holds x in the carrier of ( product (X --> Y)) & x is Function of X, the carrier of Y

    proof

      let X be set, Y be non empty RelStr, x be Element of (Y |^ X);

      x in the carrier of (Y |^ X);

      then x in ( Funcs (X,the carrier of Y)) by Th28;

      hence thesis by FUNCT_2: 66;

    end;

    registration

      let X be set;

      let Y be reflexive non empty RelStr;

      cluster (Y |^ X) -> reflexive;

      coherence

      proof

        per cases ;

          suppose X is empty;

          hence thesis by Th26;

        end;

          suppose X is non empty;

          then

          reconsider X as non empty set;

          for x be Element of (Y |^ X) holds x <= x

          proof

            let x be Element of (Y |^ X);

            reconsider x1 = x as Function of X, the carrier of Y by Lm5;

            reconsider x9 = x as Element of ( product (X --> Y));



             A1: ex f,g be Function st f = x9 & g = x9 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

            proof

              take x1, x1;

              thus x1 = x9 & x1 = x9;

              let i be object;

              assume i in X;

              then

              reconsider i as Element of X;

              take R = ((X --> Y) . i);

              reconsider xi = (x1 . i), yi = (x1 . i) as Element of R;

              take xi, yi;

              reconsider xi1 = xi, yi1 = xi as Element of Y;

              xi1 <= yi1;

              hence thesis;

            end;

            x in the carrier of ( product (X --> Y));

            then x9 in ( product ( Carrier (X --> Y))) by Def4;

            hence thesis by A1, Def4;

          end;

          hence thesis by YELLOW_0:def 1;

        end;

      end;

    end

    registration

      let Y be non empty RelStr;

      cluster (Y |^ {} ) -> 1 -element;

      coherence by Th26;

    end

    registration

      let Y be non empty reflexive RelStr;

      cluster (Y |^ {} ) -> with_infima with_suprema antisymmetric;

      coherence ;

    end

    registration

      let X be set;

      let Y be transitive non empty RelStr;

      cluster (Y |^ X) -> transitive;

      coherence

      proof

        set IT = (Y |^ X);

        now

          let x,y,z be Element of IT;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( product (X --> Y));

          assume that

           A1: x <= y and

           A2: y <= z;

          y1 in the carrier of ( product (X --> Y));

          then y1 in ( product ( Carrier (X --> Y))) by Def4;

          then

          consider f1,g1 be Function such that

           A3: f1 = y1 & g1 = z1 and

           A4: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A2, Def4;

          x1 in the carrier of ( product (X --> Y));

          then

           A5: x1 in ( product ( Carrier (X --> Y))) by Def4;

          then

          consider f,g be Function such that

           A6: f = x1 & g = y1 and

           A7: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A1, Def4;

          ex f2,g2 be Function st f2 = x1 & g2 = z1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f2 . i) & yi = (g2 . i) & xi <= yi

          proof

            reconsider f2 = x, g2 = z as Function of X, the carrier of Y by Lm5;

            take f2, g2;

            thus f2 = x1 & g2 = z1;

            let i be object;

            assume

             A8: i in X;

            then

            reconsider X as non empty set;

            reconsider i as Element of X by A8;

            reconsider R = ((X --> Y) . i) as RelStr;

            reconsider xi = (f2 . i), yi = (g2 . i) as Element of R by FUNCT_2: 5;

            take R, xi, yi;

            (ex R1 be RelStr, xi1,yi1 be Element of R1 st R1 = ((X --> Y) . i) & xi1 = (f . i) & yi1 = (g . i) & xi1 <= yi1) & ex R2 be RelStr, xi2,yi2 be Element of R2 st R2 = ((X --> Y) . i) & xi2 = (f1 . i) & yi2 = (g1 . i) & xi2 <= yi2 by A7, A4;

            hence thesis by A6, A3, YELLOW_0:def 2;

          end;

          hence x <= z by A5, Def4;

        end;

        hence thesis by YELLOW_0:def 2;

      end;

    end

    registration

      let X be set;

      let Y be antisymmetric non empty RelStr;

      cluster (Y |^ X) -> antisymmetric;

      coherence

      proof

        set IT = (Y |^ X);

        now

          let x,y be Element of IT;

          reconsider x19 = x, y19 = y as Function of X, the carrier of Y by Lm5;

          reconsider x1 = x, y1 = y as Element of ( product (X --> Y));

          assume that

           A1: x <= y and

           A2: y <= x;

          y1 in the carrier of ( product (X --> Y));

          then y1 in ( product ( Carrier (X --> Y))) by Def4;

          then

          consider f1,g1 be Function such that

           A3: f1 = y1 & g1 = x1 and

           A4: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A2, Def4;

          x1 in the carrier of ( product (X --> Y));

          then x1 in ( product ( Carrier (X --> Y))) by Def4;

          then

          consider f,g be Function such that

           A5: f = x1 & g = y1 and

           A6: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A1, Def4;

           A7:

          now

            let i be object;

            assume

             A8: i in X;

            then

            consider R2 be RelStr, xi2,yi2 be Element of R2 such that

             A9: R2 = ((X --> Y) . i) and

             A10: xi2 = (f1 . i) & yi2 = (g1 . i) & xi2 <= yi2 by A4;



             A11: Y = R2 by A8, A9, FUNCOP_1: 7;

            consider R1 be RelStr, xi1,yi1 be Element of R1 such that

             A12: R1 = ((X --> Y) . i) and

             A13: xi1 = (f . i) & yi1 = (g . i) & xi1 <= yi1 by A6, A8;

            Y = R1 by A8, A12, FUNCOP_1: 7;

            hence (x19 . i) = (y19 . i) by A5, A3, A13, A10, A11, ORDERS_2: 2;

          end;

          ( dom x19) = X & ( dom y19) = X by FUNCT_2:def 1;

          hence x = y by A7, FUNCT_1: 2;

        end;

        hence thesis by YELLOW_0:def 3;

      end;

    end

    registration

      let X be non empty set;

      let Y be non empty with_infima antisymmetric RelStr;

      cluster (Y |^ X) -> with_infima;

      coherence

      proof

        set IT = (Y |^ X);

        let x,y be Element of IT;

        reconsider y9 = y as Function of X, the carrier of Y by Lm5;

        reconsider x9 = x as Function of X, the carrier of Y by Lm5;

        defpred P[ object, object] means ex xa,ya be Element of Y st xa = (x9 . $1) & ya = (y9 . $1) & $2 = (xa "/\" ya);



         A1: for x be object st x in X holds ex y be object st y in the carrier of Y & P[x, y]

        proof

          let a be object;

          assume a in X;

          then

          reconsider xa = (x9 . a), ya = (y9 . a) as Element of Y by FUNCT_2: 5;

          take y = (xa "/\" ya);

          thus y in the carrier of Y;

          take xa, ya;

          thus thesis;

        end;

        consider f be Function of X, the carrier of Y such that

         A2: for a be object st a in X holds P[a, (f . a)] from FUNCT_2:sch 1( A1);

        f in ( Funcs (X,the carrier of Y)) by FUNCT_2: 8;

        then

        reconsider z = f as Element of IT by Th28;

        take z;



         A3: z <= y

        proof

          reconsider y1 = y, z1 = z as Element of ( product (X --> Y));



           A4: ex f,g be Function st f = z1 & g = y1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

          proof

            take f, y9;

            thus f = z1 & y9 = y1;

            let i be object;

            assume i in X;

            then

            reconsider i as Element of X;

            reconsider R = ((X --> Y) . i) as RelStr;

            reconsider xi = (f . i), yi = (y9 . i) as Element of R;

            take R, xi, yi;

            R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "/\" ya) by A2;

            hence thesis by YELLOW_0: 23;

          end;

          z1 in the carrier of ( product (X --> Y));

          then z1 in ( product ( Carrier (X --> Y))) by Def4;

          hence thesis by A4, Def4;

        end;



         A5: for z9 be Element of IT st z9 <= x & z9 <= y holds z9 <= z

        proof

          let z9 be Element of IT;

          assume that

           A6: z9 <= x and

           A7: z9 <= y;

          z9 <= z

          proof

            reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of ( product (X --> Y));

            reconsider J = z2, K = z3 as Function of X, the carrier of Y by Lm5;

            z9 in the carrier of ( product (X --> Y));

            then

             A8: z2 in ( product ( Carrier (X --> Y))) by Def4;

            then

            consider f1,g1 be Function such that

             A9: f1 = z2 & g1 = z5 and

             A10: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A6, Def4;

            consider f2,g2 be Function such that

             A11: f2 = z2 & g2 = z4 and

             A12: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f2 . i) & yi = (g2 . i) & xi <= yi by A7, A8, Def4;

            ex f,g be Function st f = z2 & g = z3 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

            proof

              take J, K;

              thus J = z2 & K = z3;

              let i be object;

              assume i in X;

              then

              reconsider i as Element of X;

              reconsider R = ((X --> Y) . i) as RelStr;

              reconsider xi = (J . i), yi = (K . i) as Element of R;

              take R, xi, yi;



               A13: R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "/\" ya) by A2;

              (ex R1 be RelStr, xi1,yi1 be Element of R1 st R1 = ((X --> Y) . i) & xi1 = (f1 . i) & yi1 = (g1 . i) & xi1 <= yi1) & ex R2 be RelStr, xi2,yi2 be Element of R2 st R2 = ((X --> Y) . i) & xi2 = (f2 . i) & yi2 = (g2 . i) & xi2 <= yi2 by A10, A12;

              hence thesis by A9, A11, A13, YELLOW_0: 23;

            end;

            hence thesis by A8, Def4;

          end;

          hence thesis;

        end;

        z <= x

        proof

          reconsider x1 = x, z1 = z as Element of ( product (X --> Y));



           A14: ex f,g be Function st f = z1 & g = x1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

          proof

            take f, x9;

            thus f = z1 & x9 = x1;

            let i be object;

            assume i in X;

            then

            reconsider i as Element of X;

            reconsider R = ((X --> Y) . i) as RelStr;

            reconsider xi = (f . i), yi = (x9 . i) as Element of R;

            take R, xi, yi;

            R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "/\" ya) by A2;

            hence thesis by YELLOW_0: 23;

          end;

          z1 in the carrier of ( product (X --> Y));

          then z1 in ( product ( Carrier (X --> Y))) by Def4;

          hence thesis by A14, Def4;

        end;

        hence thesis by A3, A5;

      end;

    end

    registration

      let X be non empty set;

      let Y be non empty with_suprema antisymmetric RelStr;

      cluster (Y |^ X) -> with_suprema;

      coherence

      proof

        set IT = (Y |^ X);

        let x,y be Element of IT;

        reconsider y9 = y as Function of X, the carrier of Y by Lm5;

        reconsider x9 = x as Function of X, the carrier of Y by Lm5;

        defpred P[ object, object] means ex xa,ya be Element of Y st xa = (x9 . $1) & ya = (y9 . $1) & $2 = (xa "\/" ya);



         A1: for x be object st x in X holds ex y be object st y in the carrier of Y & P[x, y]

        proof

          let a be object;

          assume a in X;

          then

          reconsider xa = (x9 . a), ya = (y9 . a) as Element of Y by FUNCT_2: 5;

          take y = (xa "\/" ya);

          thus y in the carrier of Y;

          take xa, ya;

          thus thesis;

        end;

        consider f be Function of X, the carrier of Y such that

         A2: for a be object st a in X holds P[a, (f . a)] from FUNCT_2:sch 1( A1);

        f in ( Funcs (X,the carrier of Y)) by FUNCT_2: 8;

        then

        reconsider z = f as Element of IT by Th28;

        take z;



         A3: y <= z

        proof

          reconsider y1 = y, z1 = z as Element of ( product (X --> Y));



           A4: ex f,g be Function st f = y1 & g = z1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

          proof

            take y9, f;

            thus y9 = y1 & f = z1;

            let i be object;

            assume i in X;

            then

            reconsider i as Element of X;

            reconsider R = ((X --> Y) . i) as RelStr;

            reconsider yi = (f . i), xi = (y9 . i) as Element of R;

            take R, xi, yi;

            R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "\/" ya) by A2;

            hence thesis by YELLOW_0: 22;

          end;

          y1 in the carrier of ( product (X --> Y));

          then y1 in ( product ( Carrier (X --> Y))) by Def4;

          hence thesis by A4, Def4;

        end;



         A5: for z9 be Element of IT st z9 >= x & z9 >= y holds z9 >= z

        proof

          let z9 be Element of IT;

          assume that

           A6: z9 >= x and

           A7: z9 >= y;

          z9 >= z

          proof

            reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of ( product (X --> Y));

            z4 in the carrier of ( product (X --> Y));

            then z4 in ( product ( Carrier (X --> Y))) by Def4;

            then

            consider f2,g2 be Function such that

             A8: f2 = z4 & g2 = z2 and

             A9: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f2 . i) & yi = (g2 . i) & xi <= yi by A7, Def4;

            reconsider K = z3, J = z2 as Function of X, the carrier of Y by Lm5;

            z5 in the carrier of ( product (X --> Y));

            then z5 in ( product ( Carrier (X --> Y))) by Def4;

            then

            consider f1,g1 be Function such that

             A10: f1 = z5 & g1 = z2 and

             A11: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A6, Def4;



             A12: ex f,g be Function st f = z3 & g = z2 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

            proof

              take K, J;

              thus K = z3 & J = z2;

              let i be object;

              assume i in X;

              then

              reconsider i as Element of X;

              reconsider R = ((X --> Y) . i) as RelStr;

              reconsider yi = (J . i), xi = (K . i) as Element of R;

              take R, xi, yi;



               A13: R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "\/" ya) by A2;

              (ex R1 be RelStr, xi1,yi1 be Element of R1 st R1 = ((X --> Y) . i) & xi1 = (f1 . i) & yi1 = (g1 . i) & xi1 <= yi1) & ex R2 be RelStr, xi2,yi2 be Element of R2 st R2 = ((X --> Y) . i) & xi2 = (f2 . i) & yi2 = (g2 . i) & xi2 <= yi2 by A11, A9;

              hence thesis by A10, A8, A13, YELLOW_0: 22;

            end;

            z3 in the carrier of ( product (X --> Y));

            then z3 in ( product ( Carrier (X --> Y))) by Def4;

            hence thesis by A12, Def4;

          end;

          hence thesis;

        end;

        x <= z

        proof

          reconsider x1 = x, z1 = z as Element of ( product (X --> Y));



           A14: ex f,g be Function st f = x1 & g = z1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = ((X --> Y) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

          proof

            take x9, f;

            thus x9 = x1 & f = z1;

            let i be object;

            assume i in X;

            then

            reconsider i as Element of X;

            reconsider R = ((X --> Y) . i) as RelStr;

            reconsider yi = (f . i), xi = (x9 . i) as Element of R;

            take R, xi, yi;

            R = Y & ex xa,ya be Element of Y st xa = (x9 . i) & ya = (y9 . i) & (f . i) = (xa "\/" ya) by A2;

            hence thesis by YELLOW_0: 22;

          end;

          x1 in the carrier of ( product (X --> Y));

          then x1 in ( product ( Carrier (X --> Y))) by Def4;

          hence thesis by A14, Def4;

        end;

        hence thesis by A3, A5;

      end;

    end

    definition

      let S,T be RelStr;

      :: YELLOW_1:def6

      func MonMaps (S,T) -> strict full SubRelStr of (T |^ the carrier of S) means for f be Function of S, T holds f in the carrier of it iff f in ( Funcs (the carrier of S,the carrier of T)) & f is monotone;

      existence

      proof

        set X = ( MonFuncs (S,T));

        X c= ( Funcs (the carrier of S,the carrier of T)) by ORDERS_3: 11;

        then

        reconsider X as Subset of (T |^ the carrier of S) by Th28;

        take SX = ( subrelstr X);

        let f be Function of S, T;

        hereby

          assume f in the carrier of SX;

          then f in X by YELLOW_0:def 15;

          then ex f9 be Function of S, T st f9 = f & f9 in ( Funcs (the carrier of S,the carrier of T)) & f9 is monotone by ORDERS_3:def 6;

          hence f in ( Funcs (the carrier of S,the carrier of T)) & f is monotone;

        end;

        assume f in ( Funcs (the carrier of S,the carrier of T)) & f is monotone;

        then f in X by ORDERS_3:def 6;

        hence thesis by YELLOW_0:def 15;

      end;

      uniqueness

      proof

        let A1,A2 be strict full SubRelStr of (T |^ the carrier of S);

        assume that

         A1: for f be Function of S, T holds f in the carrier of A1 iff f in ( Funcs (the carrier of S,the carrier of T)) & f is monotone and

         A2: for f be Function of S, T holds f in the carrier of A2 iff f in ( Funcs (the carrier of S,the carrier of T)) & f is monotone;

        the carrier of A2 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;

        then

         A3: the carrier of A2 c= ( Funcs (the carrier of S,the carrier of T)) by Th28;



         A4: the carrier of A2 c= the carrier of A1

        proof

          let a be object;

          assume

           A5: a in the carrier of A2;

          then

          reconsider f = a as Function of S, T by A3, FUNCT_2: 66;

          f is monotone by A2, A5;

          hence thesis by A1, A3, A5;

        end;

        the carrier of A1 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;

        then

         A6: the carrier of A1 c= ( Funcs (the carrier of S,the carrier of T)) by Th28;

        the carrier of A1 c= the carrier of A2

        proof

          let a be object;

          assume

           A7: a in the carrier of A1;

          then

          reconsider f = a as Function of S, T by A6, FUNCT_2: 66;

          f is monotone by A1, A7;

          hence thesis by A2, A6, A7;

        end;

        then the carrier of A1 = the carrier of A2 by A4;

        hence thesis by YELLOW_0: 57;

      end;

    end