real_lat.miz



    begin

    reserve x,y for Real;

    definition

      :: REAL_LAT:def1

      func minreal -> BinOp of REAL means

      : Def1: (it . (x,y)) = ( min (x,y));

      existence

      proof

        deffunc F( Real, Real) = ( In (( min ($1,$2)), REAL ));

        consider o be BinOp of REAL such that

         A1: for a,b be Element of REAL holds (o . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take o;

        let a,b be Real;

        reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

        (o . (aa,bb)) = F(aa,bb) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of REAL ;

        assume that

         A2: (f1 . (x,y)) = ( min (x,y)) and

         A3: (f2 . (x,y)) = ( min (x,y));

        for x,y be Element of REAL holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Element of REAL ;

          (f1 . (x,y)) = ( min (x,y)) by A2;

          hence thesis by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: REAL_LAT:def2

      func maxreal -> BinOp of REAL means

      : Def2: (it . (x,y)) = ( max (x,y));

      existence

      proof

        deffunc F( Real, Real) = ( In (( max ($1,$2)), REAL ));

        consider o be BinOp of REAL such that

         A4: for a,b be Element of REAL holds (o . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take o;

        let a,b be Real;

        reconsider a, b as Element of REAL by XREAL_0:def 1;

        (o . (a,b)) = F(a,b) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of REAL ;

        assume that

         A5: (f1 . (x,y)) = ( max (x,y)) and

         A6: (f2 . (x,y)) = ( max (x,y));

        for x,y be Element of REAL holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be Element of REAL ;

          (f1 . (x,y)) = ( max (x,y)) by A5;

          hence thesis by A6;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      :: REAL_LAT:def3

      func Real_Lattice -> strict LattStr equals LattStr (# REAL , maxreal , minreal #);

      coherence ;

    end

    registration

      cluster the carrier of Real_Lattice -> real-membered;

      coherence ;

    end

    registration

      cluster Real_Lattice -> non empty;

      coherence ;

    end

    reserve a,b,c for Element of Real_Lattice ;

    registration

      let a,b be Element of Real_Lattice ;

      identify max (a,b) with a "\/" b;

      compatibility by Def2;

      identify min (a,b) with a "/\" b;

      compatibility by Def1;

    end

    

     Lm1: (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by XXREAL_0: 34;

    

     Lm2: ((a "/\" b) "\/" b) = b by XXREAL_0: 36;

    

     Lm3: (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by XXREAL_0: 33;

    

     Lm4: (a "/\" (a "\/" b)) = a by XXREAL_0: 35;

    registration

      cluster Real_Lattice -> Lattice-like;

      coherence

      proof

         Real_Lattice is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by Lm1, Lm2, Lm3, Lm4;

        hence thesis;

      end;

    end

    

     Lm5: (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c)) by XXREAL_0: 38;

    reserve p,q,r for Element of Real_Lattice ;

    theorem :: REAL_LAT:1

    

     Th1: ( maxreal . (p,q)) = ( maxreal . (q,p))

    proof

      

      thus ( maxreal . (p,q)) = (q "\/" p) by LATTICES:def 1

      .= ( maxreal . (q,p));

    end;

    theorem :: REAL_LAT:2

    

     Th2: ( minreal . (p,q)) = ( minreal . (q,p))

    proof

      

      thus ( minreal . (p,q)) = (q "/\" p) by LATTICES:def 2

      .= ( minreal . (q,p));

    end;

    theorem :: REAL_LAT:3

    

     Th3: ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (q,r)),p)) & ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (p,q)),r)) & ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (q,p)),r)) & ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (r,p)),q)) & ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (r,q)),p)) & ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (p,r)),q))

    proof

      set s = (q "\/" r);

      

      thus

       A1: ( maxreal . (p,( maxreal . (q,r)))) = (s "\/" p) by LATTICES:def 1

      .= ( maxreal . (( maxreal . (q,r)),p));

      

      thus ( maxreal . (p,( maxreal . (q,r)))) = (p "\/" s)

      .= ((p "\/" q) "\/" r) by XXREAL_0: 34

      .= ( maxreal . (( maxreal . (p,q)),r));

      

      thus ( maxreal . (p,( maxreal . (q,r)))) = (p "\/" s)

      .= ((q "\/" p) "\/" r) by XXREAL_0: 34

      .= ( maxreal . (( maxreal . (q,p)),r));

      

      thus

       A2: ( maxreal . (p,( maxreal . (q,r)))) = (p "\/" (q "\/" r))

      .= ((r "\/" p) "\/" q) by XXREAL_0: 34

      .= ( maxreal . (( maxreal . (r,p)),q));

      thus ( maxreal . (p,( maxreal . (q,r)))) = ( maxreal . (( maxreal . (r,q)),p)) by A1, Th1;

      thus thesis by A2, Th1;

    end;

    theorem :: REAL_LAT:4

    

     Th4: ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (q,r)),p)) & ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (p,q)),r)) & ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (q,p)),r)) & ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (r,p)),q)) & ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (r,q)),p)) & ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (p,r)),q))

    proof

      set s = (q "/\" r);

      

      thus

       A1: ( minreal . (p,( minreal . (q,r)))) = (s "/\" p) by LATTICES:def 2

      .= ( minreal . (( minreal . (q,r)),p));

      

      thus ( minreal . (p,( minreal . (q,r)))) = (p "/\" s)

      .= ((p "/\" q) "/\" r) by XXREAL_0: 33

      .= ( minreal . (( minreal . (p,q)),r));

      

      thus ( minreal . (p,( minreal . (q,r)))) = (p "/\" s)

      .= ((q "/\" p) "/\" r) by XXREAL_0: 33

      .= ( minreal . (( minreal . (q,p)),r));

      

      thus

       A2: ( minreal . (p,( minreal . (q,r)))) = (p "/\" (q "/\" r))

      .= ((r "/\" p) "/\" q) by XXREAL_0: 33

      .= ( minreal . (( minreal . (r,p)),q));

      thus ( minreal . (p,( minreal . (q,r)))) = ( minreal . (( minreal . (r,q)),p)) by A1, Th2;

      thus thesis by A2, Th2;

    end;

    theorem :: REAL_LAT:5

    

     Th5: ( maxreal . (( minreal . (p,q)),q)) = q & ( maxreal . (q,( minreal . (p,q)))) = q & ( maxreal . (q,( minreal . (q,p)))) = q & ( maxreal . (( minreal . (q,p)),q)) = q

    proof

      set s = (p "/\" q);

      

      thus

       A1: ( maxreal . (( minreal . (p,q)),q)) = (s "\/" q)

      .= q by XXREAL_0: 36;

      

      thus ( maxreal . (q,( minreal . (p,q)))) = ((p "/\" q) "\/" q) by LATTICES:def 1

      .= q by XXREAL_0: 36;

      

      thus ( maxreal . (q,( minreal . (q,p)))) = ( maxreal . (q,(q "/\" p)))

      .= ((p "/\" q) "\/" q) by LATTICES:def 1

      .= q by XXREAL_0: 36;

      thus thesis by A1, Th2;

    end;

    theorem :: REAL_LAT:6

    

     Th6: ( minreal . (q,( maxreal . (q,p)))) = q & ( minreal . (( maxreal . (p,q)),q)) = q & ( minreal . (q,( maxreal . (p,q)))) = q & ( minreal . (( maxreal . (q,p)),q)) = q

    proof

      set s = (q "\/" p);

      

      thus

       A1: ( minreal . (q,( maxreal . (q,p)))) = (q "/\" s)

      .= q by XXREAL_0: 35;

      

      thus

       A2: ( minreal . (( maxreal . (p,q)),q)) = ( minreal . ((p "\/" q),q))

      .= (q "/\" (q "\/" p)) by LATTICES:def 2

      .= q by XXREAL_0: 35;

      thus ( minreal . (q,( maxreal . (p,q)))) = q by A1, Th1;

      thus thesis by A2, Th1;

    end;

    theorem :: REAL_LAT:7

    

     Th7: ( minreal . (q,( maxreal . (p,r)))) = ( maxreal . (( minreal . (q,p)),( minreal . (q,r))))

    proof

      set s = (p "\/" r);

      

      thus ( minreal . (q,( maxreal . (p,r)))) = (q "/\" s)

      .= ((q "/\" p) "\/" (q "/\" r)) by XXREAL_0: 38

      .= ( maxreal . (( minreal . (q,p)),( minreal . (q,r))));

    end;

    registration

      cluster Real_Lattice -> distributive;

      coherence by Lm5;

    end

    reserve A,B for non empty set;

    reserve f,g,h for Element of ( Funcs (A, REAL ));

    definition

      let A;

      :: REAL_LAT:def4

      func maxfuncreal (A) -> BinOp of ( Funcs (A, REAL )) means

      : Def4: (it . (f,g)) = ( maxreal .: (f,g));

      existence

      proof

        deffunc O( Element of ( Funcs (A, REAL )), Element of ( Funcs (A, REAL ))) = ( maxreal .: ($1,$2));

        ex o be BinOp of ( Funcs (A, REAL )) st for a,b be Element of ( Funcs (A, REAL )) holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( Funcs (A, REAL )) such that

         A1: for f,g be Element of ( Funcs (A, REAL )) holds (F1 . (f,g)) = ( maxreal .: (f,g)) and

         A2: for f,g be Element of ( Funcs (A, REAL )) holds (F2 . (f,g)) = ( maxreal .: (f,g));

        now

          let f,g be Element of ( Funcs (A, REAL ));

          

          thus (F1 . (f,g)) = ( maxreal .: (f,g)) by A1

          .= (F2 . (f,g)) by A2;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: REAL_LAT:def5

      func minfuncreal (A) -> BinOp of ( Funcs (A, REAL )) means

      : Def5: (it . (f,g)) = ( minreal .: (f,g));

      existence

      proof

        deffunc O( Element of ( Funcs (A, REAL )), Element of ( Funcs (A, REAL ))) = ( minreal .: ($1,$2));

        ex o be BinOp of ( Funcs (A, REAL )) st for a,b be Element of ( Funcs (A, REAL )) holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( Funcs (A, REAL )) such that

         A3: for f,g be Element of ( Funcs (A, REAL )) holds (F1 . (f,g)) = ( minreal .: (f,g)) and

         A4: for f,g be Element of ( Funcs (A, REAL )) holds (F2 . (f,g)) = ( minreal .: (f,g));

        now

          let f,g be Element of ( Funcs (A, REAL ));

          

          thus (F1 . (f,g)) = ( minreal .: (f,g)) by A3

          .= (F2 . (f,g)) by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    

     Lm6: for x be Element of A, f be Function of A, B holds x in ( dom f)

    proof

      let x be Element of A, f be Function of A, B;

      x in A;

      hence thesis by FUNCT_2:def 1;

    end;

    theorem :: REAL_LAT:8

    

     Th8: (( maxfuncreal A) . (f,g)) = (( maxfuncreal A) . (g,f))

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( maxreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( maxreal .: (g,f))) by Lm6;

        

        thus ((( maxfuncreal A) . (f,g)) . x) = (( maxreal .: (f,g)) . x) by Def4

        .= ( maxreal . ((f . x),(g . x))) by A1, FUNCOP_1: 22

        .= ( maxreal . ((g . x),(f . x))) by Th1

        .= (( maxreal .: (g,f)) . x) by A2, FUNCOP_1: 22

        .= ((( maxfuncreal A) . (g,f)) . x) by Def4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:9

    

     Th9: (( minfuncreal A) . (f,g)) = (( minfuncreal A) . (g,f))

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( minreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( minreal .: (g,f))) by Lm6;

        

        thus ((( minfuncreal A) . (f,g)) . x) = (( minreal .: (f,g)) . x) by Def5

        .= ( minreal . ((f . x),(g . x))) by A1, FUNCOP_1: 22

        .= ( minreal . ((g . x),(f . x))) by Th2

        .= (( minreal .: (g,f)) . x) by A2, FUNCOP_1: 22

        .= ((( minfuncreal A) . (g,f)) . x) by Def5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:10

    

     Th10: (( maxfuncreal A) . ((( maxfuncreal A) . (f,g)),h)) = (( maxfuncreal A) . (f,(( maxfuncreal A) . (g,h))))

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( maxreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( maxreal .: (g,h))) by Lm6;

        

         A3: x in ( dom ( maxreal .: (( maxreal .: (f,g)),h))) by Lm6;

        

         A4: x in ( dom ( maxreal .: (f,( maxreal .: (g,h))))) by Lm6;

        

        thus ((( maxfuncreal A) . ((( maxfuncreal A) . (f,g)),h)) . x) = ((( maxfuncreal A) . (( maxreal .: (f,g)),h)) . x) by Def4

        .= (( maxreal .: (( maxreal .: (f,g)),h)) . x) by Def4

        .= ( maxreal . ((( maxreal .: (f,g)) . x),(h . x))) by A3, FUNCOP_1: 22

        .= ( maxreal . (( maxreal . ((f . x),(g . x))),(h . x))) by A1, FUNCOP_1: 22

        .= ( maxreal . ((f . x),( maxreal . ((g . x),(h . x))))) by Th3

        .= ( maxreal . ((f . x),(( maxreal .: (g,h)) . x))) by A2, FUNCOP_1: 22

        .= (( maxreal .: (f,( maxreal .: (g,h)))) . x) by A4, FUNCOP_1: 22

        .= ((( maxfuncreal A) . (f,( maxreal .: (g,h)))) . x) by Def4

        .= ((( maxfuncreal A) . (f,(( maxfuncreal A) . (g,h)))) . x) by Def4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:11

    

     Th11: (( minfuncreal A) . ((( minfuncreal A) . (f,g)),h)) = (( minfuncreal A) . (f,(( minfuncreal A) . (g,h))))

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( minreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( minreal .: (g,h))) by Lm6;

        

         A3: x in ( dom ( minreal .: (( minreal .: (f,g)),h))) by Lm6;

        

         A4: x in ( dom ( minreal .: (f,( minreal .: (g,h))))) by Lm6;

        

        thus ((( minfuncreal A) . ((( minfuncreal A) . (f,g)),h)) . x) = ((( minfuncreal A) . (( minreal .: (f,g)),h)) . x) by Def5

        .= (( minreal .: (( minreal .: (f,g)),h)) . x) by Def5

        .= ( minreal . ((( minreal .: (f,g)) . x),(h . x))) by A3, FUNCOP_1: 22

        .= ( minreal . (( minreal . ((f . x),(g . x))),(h . x))) by A1, FUNCOP_1: 22

        .= ( minreal . ((f . x),( minreal . ((g . x),(h . x))))) by Th4

        .= ( minreal . ((f . x),(( minreal .: (g,h)) . x))) by A2, FUNCOP_1: 22

        .= (( minreal .: (f,( minreal .: (g,h)))) . x) by A4, FUNCOP_1: 22

        .= ((( minfuncreal A) . (f,( minreal .: (g,h)))) . x) by Def5

        .= ((( minfuncreal A) . (f,(( minfuncreal A) . (g,h)))) . x) by Def5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:12

    

     Th12: (( maxfuncreal A) . (f,(( minfuncreal A) . (f,g)))) = f

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( minreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( maxreal .: (f,( minreal .: (f,g))))) by Lm6;

        

        thus ((( maxfuncreal A) . (f,(( minfuncreal A) . (f,g)))) . x) = ((( maxfuncreal A) . (f,( minreal .: (f,g)))) . x) by Def5

        .= (( maxreal .: (f,( minreal .: (f,g)))) . x) by Def4

        .= ( maxreal . ((f . x),(( minreal .: (f,g)) . x))) by A2, FUNCOP_1: 22

        .= ( maxreal . ((f . x),( minreal . ((f . x),(g . x))))) by A1, FUNCOP_1: 22

        .= (f . x) by Th5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:13

    

     Th13: (( maxfuncreal A) . ((( minfuncreal A) . (f,g)),f)) = f

    proof

      

      thus (( maxfuncreal A) . ((( minfuncreal A) . (f,g)),f)) = (( maxfuncreal A) . (f,(( minfuncreal A) . (f,g)))) by Th8

      .= f by Th12;

    end;

    theorem :: REAL_LAT:14

    

     Th14: (( maxfuncreal A) . ((( minfuncreal A) . (g,f)),f)) = f

    proof

      

      thus (( maxfuncreal A) . ((( minfuncreal A) . (g,f)),f)) = (( maxfuncreal A) . ((( minfuncreal A) . (f,g)),f)) by Th9

      .= f by Th13;

    end;

    theorem :: REAL_LAT:15

    (( maxfuncreal A) . (f,(( minfuncreal A) . (g,f)))) = f

    proof

      

      thus (( maxfuncreal A) . (f,(( minfuncreal A) . (g,f)))) = (( maxfuncreal A) . (f,(( minfuncreal A) . (f,g)))) by Th9

      .= f by Th12;

    end;

    theorem :: REAL_LAT:16

    

     Th16: (( minfuncreal A) . (f,(( maxfuncreal A) . (f,g)))) = f

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( maxreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( minreal .: (f,( maxreal .: (f,g))))) by Lm6;

        

        thus ((( minfuncreal A) . (f,(( maxfuncreal A) . (f,g)))) . x) = ((( minfuncreal A) . (f,( maxreal .: (f,g)))) . x) by Def4

        .= (( minreal .: (f,( maxreal .: (f,g)))) . x) by Def5

        .= ( minreal . ((f . x),(( maxreal .: (f,g)) . x))) by A2, FUNCOP_1: 22

        .= ( minreal . ((f . x),( maxreal . ((f . x),(g . x))))) by A1, FUNCOP_1: 22

        .= (f . x) by Th6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: REAL_LAT:17

    

     Th17: (( minfuncreal A) . (f,(( maxfuncreal A) . (g,f)))) = f

    proof

      

      thus (( minfuncreal A) . (f,(( maxfuncreal A) . (g,f)))) = (( minfuncreal A) . (f,(( maxfuncreal A) . (f,g)))) by Th8

      .= f by Th16;

    end;

    theorem :: REAL_LAT:18

    

     Th18: (( minfuncreal A) . ((( maxfuncreal A) . (g,f)),f)) = f

    proof

      

      thus (( minfuncreal A) . ((( maxfuncreal A) . (g,f)),f)) = (( minfuncreal A) . (f,(( maxfuncreal A) . (g,f)))) by Th9

      .= f by Th17;

    end;

    theorem :: REAL_LAT:19

    (( minfuncreal A) . ((( maxfuncreal A) . (f,g)),f)) = f

    proof

      

      thus (( minfuncreal A) . ((( maxfuncreal A) . (f,g)),f)) = (( minfuncreal A) . ((( maxfuncreal A) . (g,f)),f)) by Th8

      .= f by Th18;

    end;

    theorem :: REAL_LAT:20

    

     Th20: (( minfuncreal A) . (f,(( maxfuncreal A) . (g,h)))) = (( maxfuncreal A) . ((( minfuncreal A) . (f,g)),(( minfuncreal A) . (f,h))))

    proof

      now

        let x be Element of A;

        

         A1: x in ( dom ( minreal .: (f,g))) by Lm6;

        

         A2: x in ( dom ( minreal .: (f,h))) by Lm6;

        

         A3: x in ( dom ( minreal .: (f,( maxreal .: (g,h))))) by Lm6;

        

         A4: x in ( dom ( maxreal .: (( minreal .: (f,g)),( minreal .: (f,h))))) by Lm6;

        

         A5: x in ( dom ( maxreal .: (g,h))) by Lm6;

        

        thus ((( minfuncreal A) . (f,(( maxfuncreal A) . (g,h)))) . x) = ((( minfuncreal A) . (f,( maxreal .: (g,h)))) . x) by Def4

        .= (( minreal .: (f,( maxreal .: (g,h)))) . x) by Def5

        .= ( minreal . ((f . x),(( maxreal .: (g,h)) . x))) by A3, FUNCOP_1: 22

        .= ( minreal . ((f . x),( maxreal . ((g . x),(h . x))))) by A5, FUNCOP_1: 22

        .= ( maxreal . (( minreal . ((f . x),(g . x))),( minreal . ((f . x),(h . x))))) by Th7

        .= ( maxreal . ((( minreal .: (f,g)) . x),( minreal . ((f . x),(h . x))))) by A1, FUNCOP_1: 22

        .= ( maxreal . ((( minreal .: (f,g)) . x),(( minreal .: (f,h)) . x))) by A2, FUNCOP_1: 22

        .= (( maxreal .: (( minreal .: (f,g)),( minreal .: (f,h)))) . x) by A4, FUNCOP_1: 22

        .= ((( maxfuncreal A) . (( minreal .: (f,g)),( minreal .: (f,h)))) . x) by Def4

        .= ((( maxfuncreal A) . ((( minfuncreal A) . (f,g)),( minreal .: (f,h)))) . x) by Def5

        .= ((( maxfuncreal A) . ((( minfuncreal A) . (f,g)),(( minfuncreal A) . (f,h)))) . x) by Def5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm7: for a,b,c be Element of LattStr (# ( Funcs (A, REAL )), ( maxfuncreal A), ( minfuncreal A) #) holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by Th10;

    

     Lm8: for a,b,c be Element of LattStr (# ( Funcs (A, REAL )), ( maxfuncreal A), ( minfuncreal A) #) holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by Th11;

    definition

      let A;

      :: REAL_LAT:def6

      func RealFunc_Lattice A -> non empty strict LattStr equals LattStr (# ( Funcs (A, REAL )), ( maxfuncreal A), ( minfuncreal A) #);

      coherence ;

    end

    reserve L for non empty LattStr,

p,q,r for Element of L;

    registration

      let A;

      cluster ( RealFunc_Lattice A) -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing;

      coherence by Th8, Th10, Th14, Th9, Th11, Th16;

    end

    reserve p,q,r for Element of ( RealFunc_Lattice A);

    theorem :: REAL_LAT:21

    

     Th21: (( maxfuncreal A) . (p,q)) = (( maxfuncreal A) . (q,p))

    proof

      

      thus (( maxfuncreal A) . (p,q)) = (q "\/" p) by LATTICES:def 1

      .= (( maxfuncreal A) . (q,p));

    end;

    theorem :: REAL_LAT:22

    

     Th22: (( minfuncreal A) . (p,q)) = (( minfuncreal A) . (q,p))

    proof

      

      thus (( minfuncreal A) . (p,q)) = (q "/\" p) by LATTICES:def 2

      .= (( minfuncreal A) . (q,p));

    end;

    theorem :: REAL_LAT:23

    (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (q,r)),p)) & (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (p,q)),r)) & (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (q,p)),r)) & (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (r,p)),q)) & (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (r,q)),p)) & (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (p,r)),q))

    proof

      set s = (q "\/" r);

      

      thus

       A1: (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (s "\/" p) by LATTICES:def 1

      .= (( maxfuncreal A) . ((( maxfuncreal A) . (q,r)),p));

      thus (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (p,q)),r)) by Th10;

      

      thus (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (p "\/" s)

      .= ((q "\/" p) "\/" r) by Lm7

      .= (( maxfuncreal A) . ((( maxfuncreal A) . (q,p)),r));

      

      thus

       A2: (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (p "\/" (q "\/" r))

      .= ((r "\/" p) "\/" q) by Lm7

      .= (( maxfuncreal A) . ((( maxfuncreal A) . (r,p)),q));

      thus (( maxfuncreal A) . (p,(( maxfuncreal A) . (q,r)))) = (( maxfuncreal A) . ((( maxfuncreal A) . (r,q)),p)) by A1, Th21;

      thus thesis by A2, Th21;

    end;

    theorem :: REAL_LAT:24

    (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (q,r)),p)) & (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (p,q)),r)) & (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (q,p)),r)) & (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (r,p)),q)) & (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (r,q)),p)) & (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (p,r)),q))

    proof

      set s = (q "/\" r);

      

      thus

       A1: (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (s "/\" p) by LATTICES:def 2

      .= (( minfuncreal A) . ((( minfuncreal A) . (q,r)),p));

      thus (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (p,q)),r)) by Th11;

      

      thus (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (p "/\" s)

      .= ((q "/\" p) "/\" r) by Lm8

      .= (( minfuncreal A) . ((( minfuncreal A) . (q,p)),r));

      

      thus

       A2: (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (p "/\" (q "/\" r))

      .= ((r "/\" p) "/\" q) by Lm8

      .= (( minfuncreal A) . ((( minfuncreal A) . (r,p)),q));

      thus (( minfuncreal A) . (p,(( minfuncreal A) . (q,r)))) = (( minfuncreal A) . ((( minfuncreal A) . (r,q)),p)) by A1, Th22;

      thus thesis by A2, Th22;

    end;

    theorem :: REAL_LAT:25

    (( maxfuncreal A) . ((( minfuncreal A) . (p,q)),q)) = q & (( maxfuncreal A) . (q,(( minfuncreal A) . (p,q)))) = q & (( maxfuncreal A) . (q,(( minfuncreal A) . (q,p)))) = q & (( maxfuncreal A) . ((( minfuncreal A) . (q,p)),q)) = q

    proof

      thus

       A1: (( maxfuncreal A) . ((( minfuncreal A) . (p,q)),q)) = q by Th14;

      

      thus (( maxfuncreal A) . (q,(( minfuncreal A) . (p,q)))) = ((p "/\" q) "\/" q) by LATTICES:def 1

      .= q by Th14;

      

      thus (( maxfuncreal A) . (q,(( minfuncreal A) . (q,p)))) = (( maxfuncreal A) . (q,(q "/\" p)))

      .= ((p "/\" q) "\/" q) by LATTICES:def 1

      .= q by Th14;

      thus thesis by A1, Th22;

    end;

    theorem :: REAL_LAT:26

    (( minfuncreal A) . (q,(( maxfuncreal A) . (q,p)))) = q & (( minfuncreal A) . ((( maxfuncreal A) . (p,q)),q)) = q & (( minfuncreal A) . (q,(( maxfuncreal A) . (p,q)))) = q & (( minfuncreal A) . ((( maxfuncreal A) . (q,p)),q)) = q

    proof

      thus

       A1: (( minfuncreal A) . (q,(( maxfuncreal A) . (q,p)))) = q by Th16;

      

      thus

       A2: (( minfuncreal A) . ((( maxfuncreal A) . (p,q)),q)) = (( minfuncreal A) . ((p "\/" q),q))

      .= (q "/\" (q "\/" p)) by LATTICES:def 2

      .= q by Th16;

      thus (( minfuncreal A) . (q,(( maxfuncreal A) . (p,q)))) = q by A1, Th21;

      thus thesis by A2, Th21;

    end;

    theorem :: REAL_LAT:27

    (( minfuncreal A) . (q,(( maxfuncreal A) . (p,r)))) = (( maxfuncreal A) . ((( minfuncreal A) . (q,p)),(( minfuncreal A) . (q,r)))) by Th20;

    theorem :: REAL_LAT:28

    ( RealFunc_Lattice A) is D_Lattice

    proof

      (p "/\" (q "\/" r)) = ((p "/\" q) "\/" (p "/\" r)) by Th20;

      hence thesis by LATTICES:def 11;

    end;