unialg_3.miz

    begin

    reserve U0 for Universal_Algebra,

U1 for SubAlgebra of U0,

o for operation of U0;

    definition

      let U0;

      :: UNIALG_3:def1

      mode SubAlgebra-Family of U0 -> set means

      : Def1: for U1 be set st U1 in it holds U1 is SubAlgebra of U0;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let U0;

      cluster non empty for SubAlgebra-Family of U0;

      existence

      proof

        set U1 = the SubAlgebra of U0;

        for U2 be set st U2 in {U1} holds U2 is SubAlgebra of U0 by TARSKI:def 1;

        then

        reconsider U00 = {U1} as SubAlgebra-Family of U0 by Def1;

        take U00;

        thus thesis;

      end;

    end

    definition

      let U0;

      :: original: Sub

      redefine

      func Sub (U0) -> non empty SubAlgebra-Family of U0 ;

      coherence

      proof

        ( Sub U0) is SubAlgebra-Family of U0

        proof

          let U1 be set;

          assume U1 in ( Sub U0);

          hence thesis by UNIALG_2:def 14;

        end;

        hence thesis;

      end;

      let U00 be non empty SubAlgebra-Family of U0;

      :: original: Element

      redefine

      mode Element of U00 -> SubAlgebra of U0 ;

      coherence by Def1;

    end

    definition

      let U0;

      let u be Element of ( Sub U0);

      :: UNIALG_3:def2

      func carr u -> Subset of U0 means

      : Def2: ex U1 be SubAlgebra of U0 st u = U1 & it = the carrier of U1;

      existence

      proof

        consider U1 be SubAlgebra of U0 such that

         A1: U1 = u;

        reconsider A = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;

        take A, U1;

        thus thesis by A1;

      end;

      uniqueness ;

    end

    definition

      let U0;

      :: UNIALG_3:def3

      func Carr U0 -> Function of ( Sub U0), ( bool the carrier of U0) means

      : Def3: for u be Element of ( Sub U0) holds (it . u) = ( carr u);

      existence

      proof

        deffunc F( Element of ( Sub U0)) = ( carr $1);

        ex f be Function of ( Sub U0), ( bool the carrier of U0) st for x be Element of ( Sub U0) holds (f . x) = F(x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Sub U0), ( bool the carrier of U0) such that

         A1: for u1 be Element of ( Sub U0) holds (F1 . u1) = ( carr u1) and

         A2: for u2 be Element of ( Sub U0) holds (F2 . u2) = ( carr u2);

        for u be object st u in ( Sub U0) holds (F1 . u) = (F2 . u)

        proof

          let u be object;

          assume u in ( Sub U0);

          then

          reconsider u1 = u as Element of ( Sub U0);

          consider U1 be SubAlgebra of U0 such that u1 = U1 and

           A3: ( carr u1) = the carrier of U1 by Def2;

          (F1 . u1) = the carrier of U1 by A1, A3;

          hence thesis by A2, A3;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: UNIALG_3:1



     Th1: for u be object holds u in ( Sub U0) iff ex U1 be strict SubAlgebra of U0 st u = U1

    proof

      let u be object;

      thus u in ( Sub U0) implies ex U1 be strict SubAlgebra of U0 st u = U1

      proof

        assume u in ( Sub U0);

        then u is strict SubAlgebra of U0 by UNIALG_2:def 14;

        hence thesis;

      end;

      thus thesis by UNIALG_2:def 14;

    end;

    theorem :: UNIALG_3:2

    for H be non empty Subset of U0 holds for o holds ( arity o) = 0 implies (H is_closed_on o iff (o . {} ) in H)

    proof

      let H be non empty Subset of U0;

      let o;

      assume

       A1: ( arity o) = 0 ;

      thus H is_closed_on o implies (o . {} ) in H

      proof

        assume

         A2: H is_closed_on o;

        consider s be FinSequence of H such that

         A3: ( len s) = ( arity o) by FINSEQ_1: 19;

        s = {} by A1, A3;

        hence thesis by A2, A3;

      end;

      thus (o . {} ) in H implies H is_closed_on o

      proof

        assume

         A4: (o . {} ) in H;

        let s be FinSequence of H;

        assume ( len s) = ( arity o);

        then s = {} by A1;

        hence thesis by A4;

      end;

    end;

    theorem :: UNIALG_3:3



     Th3: for U1 be SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0

    proof

      let U1 be SubAlgebra of U0;

      the carrier of U1 is Subset of U0 by UNIALG_2:def 7;

      hence thesis;

    end;

    theorem :: UNIALG_3:4

    for H be non empty Subset of U0 holds for o holds H is_closed_on o & ( arity o) = 0 implies (o /. H) = o

    proof

      let H be non empty Subset of U0;

      let o;

      assume that

       A1: H is_closed_on o and

       A2: ( arity o) = 0 ;



       A3: ( dom o) = ( 0 -tuples_on the carrier of U0) by A2, MARGREL1: 22

      .= {( <*> the carrier of U0)} by FINSEQ_2: 94

      .= {( <*> H)}

      .= ( 0 -tuples_on H) by FINSEQ_2: 94;

      (o /. H) = (o | ( 0 -tuples_on H)) by A1, A2, UNIALG_2:def 5;

      hence thesis by A3, RELAT_1: 69;

    end;

    theorem :: UNIALG_3:5

    ( Constants U0) = { (o . {} ) where o be operation of U0 : ( arity o) = 0 }

    proof

      set S = { (o . {} ) where o be operation of U0 : ( arity o) = 0 };

      thus ( Constants U0) c= S

      proof

        let a be object;

        assume a in ( Constants U0);

        then

        consider u be Element of U0 such that

         A1: u = a and

         A2: ex o be operation of U0 st ( arity o) = 0 & u in ( rng o);

        consider o be operation of U0 such that

         A3: ( arity o) = 0 and

         A4: u in ( rng o) by A2;

        consider a2 be object such that

         A5: a2 in ( dom o) and

         A6: u = (o . a2) by A4, FUNCT_1:def 3;

        ( dom o) = ( 0 -tuples_on the carrier of U0) by A3, MARGREL1: 22;

        then a2 is Tuple of 0 , the carrier of U0 by A5, FINSEQ_2: 131;

        then

        reconsider a1 = a2 as FinSequence of the carrier of U0;

        ( len a1) = 0 by A3, A5, MARGREL1:def 25;

        then a1 = {} ;

        hence thesis by A1, A3, A6;

      end;

      thus S c= ( Constants U0)

      proof

        let a be object;

        assume a in S;

        then

        consider o be operation of U0 such that

         A7: a = (o . {} ) and

         A8: ( arity o) = 0 ;

        ( dom o) = ( 0 -tuples_on the carrier of U0) by A8, MARGREL1: 22

        .= {( <*> the carrier of U0)} by FINSEQ_2: 94;

        then ( {} the carrier of U0) in ( dom o) by TARSKI:def 1;

        then (o . ( {} the carrier of U0)) in ( rng o) by FUNCT_1:def 3;

        hence thesis by A7, A8;

      end;

    end;

    theorem :: UNIALG_3:6



     Th6: for U0 be with_const_op Universal_Algebra holds for U1 be SubAlgebra of U0 holds ( Constants U0) = ( Constants U1)

    proof

      let U0 be with_const_op Universal_Algebra;

      let U1 be SubAlgebra of U0;

      thus ( Constants U0) c= ( Constants U1)

      proof

        reconsider A = the carrier of U1 as non empty Subset of U0 by UNIALG_2:def 7;

        let a be object;



         A1: ( Constants U0) is Subset of U1 by UNIALG_2: 15;

        assume

         A2: a in ( Constants U0);

        then

        consider u be Element of U0 such that

         A3: u = a and

         A4: ex o be operation of U0 st ( arity o) = 0 & u in ( rng o);

        consider o1 be operation of U0 such that

         A5: ( arity o1) = 0 and

         A6: u in ( rng o1) by A4;



         A7: ( dom o1) = ( 0 -tuples_on the carrier of U0) by A5, MARGREL1: 22

        .= {( <*> the carrier of U0)} by FINSEQ_2: 94

        .= {( <*> A)}

        .= ( 0 -tuples_on A) by FINSEQ_2: 94;

        consider x be object such that

         A8: x in ( dom the charact of U0) and

         A9: o1 = (the charact of U0 . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A8;

        x in ( dom the charact of U1) by A8, UNIALG_2: 7;

        then

        reconsider o = (the charact of U1 . x) as operation of U1 by FUNCT_1:def 3;

        A is opers_closed by UNIALG_2:def 7;

        then

         A10: A is_closed_on o1;

        x in ( dom ( Opers (U0,A))) by A8, UNIALG_2:def 6;

        then (( Opers (U0,A)) . x) = (o1 /. A) by A9, UNIALG_2:def 6;



        then o = (o1 /. A) by UNIALG_2:def 7

        .= (o1 | ( 0 -tuples_on A)) by A5, A10, UNIALG_2:def 5

        .= o1 by A7, RELAT_1: 69;

        hence thesis by A2, A3, A5, A6, A1;

      end;

      thus ( Constants U1) c= ( Constants U0)

      proof

        reconsider A = the carrier of U1 as non empty Subset of U0 by UNIALG_2:def 7;

        let a be object;

        assume a in ( Constants U1);

        then

        consider u be Element of U1 such that

         A11: u = a and

         A12: ex o be operation of U1 st ( arity o) = 0 & u in ( rng o);

        consider o be operation of U1 such that

         A13: ( arity o) = 0 and

         A14: u in ( rng o) by A12;

        consider x be object such that

         A15: x in ( dom the charact of U1) and

         A16: o = (the charact of U1 . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A15;



         A17: x in ( dom the charact of U0) by A15, UNIALG_2: 7;

        then

        reconsider o1 = (the charact of U0 . x) as operation of U0 by FUNCT_1:def 3;

        ( len ( signature U1)) = ( len the charact of U1) by UNIALG_1:def 4;

        then

         A18: x in ( dom ( signature U1)) by A15, FINSEQ_3: 29;

        (U1,U0) are_similar by UNIALG_2: 13;

        then ( signature U0) = ( signature U1);



        then

         A19: ( arity o1) = (( signature U1) . x) by A18, UNIALG_1:def 4

        .= 0 by A13, A16, A18, UNIALG_1:def 4;



        then

         A20: ( dom o1) = ( 0 -tuples_on the carrier of U0) by MARGREL1: 22

        .= {( <*> the carrier of U0)} by FINSEQ_2: 94

        .= {( <*> A)}

        .= ( 0 -tuples_on A) by FINSEQ_2: 94;

        A is opers_closed by UNIALG_2:def 7;

        then

         A21: A is_closed_on o1;

        the carrier of U1 is Subset of U0 by UNIALG_2:def 7;

        then

         A22: u in the carrier of U0 by TARSKI:def 3;

        x in ( dom ( Opers (U0,A))) by A17, UNIALG_2:def 6;

        then (( Opers (U0,A)) . x) = (o1 /. A) by UNIALG_2:def 6;



        then o = (o1 /. A) by A16, UNIALG_2:def 7

        .= (o1 | ( 0 -tuples_on A)) by A21, A19, UNIALG_2:def 5

        .= o1 by A20, RELAT_1: 69;

        hence thesis by A11, A13, A14, A22;

      end;

    end;

    registration

      let U0 be with_const_op Universal_Algebra;

      cluster -> with_const_op for SubAlgebra of U0;

      coherence

      proof

        let U1 be SubAlgebra of U0;

        reconsider U2 = U1 as Universal_Algebra;

        set u = the Element of ( Constants U2);

        ( Constants U2) = ( Constants U0) by Th6;

        then u in ( Constants U2);

        then ex u1 be Element of U2 st u = u1 & ex o be operation of U2 st ( arity o) = 0 & u1 in ( rng o);

        hence thesis;

      end;

    end

    theorem :: UNIALG_3:7

    for U0 be with_const_op Universal_Algebra holds for U1,U2 be SubAlgebra of U0 holds ( Constants U1) = ( Constants U2)

    proof

      let U0 be with_const_op Universal_Algebra, U1,U2 be SubAlgebra of U0;

      ( Constants U0) = ( Constants U1) by Th6;

      hence thesis by Th6;

    end;

    definition

      let U0;

      :: original: Carr

      redefine

      :: UNIALG_3:def4

      func Carr U0 means

      : Def4: for u be Element of ( Sub U0), U1 be SubAlgebra of U0 st u = U1 holds (it . u) = the carrier of U1;

      compatibility

      proof

        let f be Function of ( Sub U0), ( bool the carrier of U0);

        hereby

          assume

           A1: f = ( Carr U0);

          let u be Element of ( Sub U0), U1 be SubAlgebra of U0;

          assume

           A2: u = U1;

          ex U2 be SubAlgebra of U0 st u = U2 & ( carr u) = the carrier of U2 by Def2;

          hence (f . u) = the carrier of U1 by A1, A2, Def3;

        end;

        assume

         A3: for u be Element of ( Sub U0), U1 be SubAlgebra of U0 st u = U1 holds (f . u) = the carrier of U1;

        for u1 be Element of ( Sub U0) holds (f . u1) = ( carr u1)

        proof

          let u be Element of ( Sub U0);

          reconsider U1 = u as Element of ( Sub U0);

          (f . u) = the carrier of U1 by A3;

          hence thesis by Def2;

        end;

        hence f = ( Carr U0) by Def3;

      end;

    end

    theorem :: UNIALG_3:8

    for H be strict SubAlgebra of U0 holds for u be Element of U0 holds u in (( Carr U0) . H) iff u in H

    proof

      let H be strict SubAlgebra of U0;

      let u be Element of U0;

      thus u in (( Carr U0) . H) implies u in H

      proof



         A1: H in ( Sub U0) by UNIALG_2:def 14;

        assume u in (( Carr U0) . H);

        then u in the carrier of H by A1, Def4;

        hence thesis by STRUCT_0:def 5;

      end;

      thus u in H implies u in (( Carr U0) . H)

      proof

        H in ( Sub U0) by UNIALG_2:def 14;

        then

         A2: (( Carr U0) . H) = the carrier of H by Def4;

        assume u in H;

        hence thesis by A2, STRUCT_0:def 5;

      end;

    end;

    theorem :: UNIALG_3:9



     Th9: for H be non empty Subset of ( Sub U0) holds (( Carr U0) .: H) is non empty

    proof

      let H be non empty Subset of ( Sub U0);

      consider u be Element of ( Sub U0) such that

       A1: u in H by SUBSET_1: 4;

      (( Carr U0) . u) in (( Carr U0) .: H) by A1, FUNCT_2: 35;

      hence thesis;

    end;

    theorem :: UNIALG_3:10

    for U0 be with_const_op Universal_Algebra holds for U1 be strict SubAlgebra of U0 holds ( Constants U0) c= (( Carr U0) . U1)

    proof

      let U0 be with_const_op Universal_Algebra;

      let U1 be strict SubAlgebra of U0;

      U1 in ( Sub U0) by Th1;

      then

       A1: (( Carr U0) . U1) = the carrier of U1 by Def4;

      ( Constants U1) = ( Constants U0) by Th6;

      hence thesis by A1;

    end;

    theorem :: UNIALG_3:11



     Th11: for U0 be with_const_op Universal_Algebra holds for U1 be SubAlgebra of U0 holds for a be set holds a is Element of ( Constants U0) implies a in the carrier of U1

    proof

      let U0 be with_const_op Universal_Algebra;

      let U1 be SubAlgebra of U0;

      let a be set;



       A1: ( Constants U0) is Subset of U1 by UNIALG_2: 15;

      assume a is Element of ( Constants U0);

      hence thesis by A1, TARSKI:def 3;

    end;

    theorem :: UNIALG_3:12



     Th12: for U0 be with_const_op Universal_Algebra holds for H be non empty Subset of ( Sub U0) holds ( meet (( Carr U0) .: H)) is non empty Subset of U0

    proof

      let U0 be with_const_op Universal_Algebra;

      let H be non empty Subset of ( Sub U0);

      set u = the Element of ( Constants U0);

      reconsider CH = (( Carr U0) .: H) as Subset-Family of U0;



       A1: for S be set st S in (( Carr U0) .: H) holds u in S

      proof

        let S be set;

        assume

         A2: S in (( Carr U0) .: H);

        then

        reconsider S as Subset of U0;

        consider X1 be Element of ( Sub U0) such that X1 in H and

         A3: S = (( Carr U0) . X1) by A2, FUNCT_2: 65;

        reconsider X1 as strict SubAlgebra of U0 by UNIALG_2:def 14;

        S = the carrier of X1 by A3, Def4;

        hence thesis by Th11;

      end;

      CH <> {} by Th9;

      hence thesis by A1, SETFAM_1:def 1;

    end;

    theorem :: UNIALG_3:13

    for U0 be with_const_op Universal_Algebra holds the carrier of ( UnSubAlLattice U0) = ( Sub U0);

    theorem :: UNIALG_3:14



     Th14: for U0 be with_const_op Universal_Algebra holds for H be non empty Subset of ( Sub U0) holds for S be non empty Subset of U0 st S = ( meet (( Carr U0) .: H)) holds S is opers_closed

    proof

      let U0 be with_const_op Universal_Algebra;

      let H be non empty Subset of ( Sub U0);

      let S be non empty Subset of U0 such that

       A1: S = ( meet (( Carr U0) .: H));



       A2: (( Carr U0) .: H) <> {} by Th9;

      for o be operation of U0 holds S is_closed_on o

      proof

        let o be operation of U0;

        let s be FinSequence of S;

        assume

         A3: ( len s) = ( arity o);

        now

          let a be set;

          assume

           A4: a in (( Carr U0) .: H);

          then

          reconsider H1 = a as Subset of U0;

          consider H2 be Element of ( Sub U0) such that H2 in H and

           A5: H1 = (( Carr U0) . H2) by A4, FUNCT_2: 65;



           A6: H1 = the carrier of H2 by A5, Def4;

          then

          reconsider H3 = H1 as non empty Subset of U0;

          S c= H1 by A1, A4, SETFAM_1: 3;

          then

          reconsider s1 = s as FinSequence of H3 by FINSEQ_2: 24;

          H3 is opers_closed by A6, UNIALG_2:def 7;

          then H3 is_closed_on o;

          then (o . s1) in H3 by A3;

          hence (o . s) in a;

        end;

        hence thesis by A1, A2, SETFAM_1:def 1;

      end;

      hence thesis;

    end;

    definition

      let U0 be with_const_op strict Universal_Algebra;

      let H be non empty Subset of ( Sub U0);

      :: UNIALG_3:def5

      func meet H -> strict SubAlgebra of U0 means

      : Def5: the carrier of it = ( meet (( Carr U0) .: H));

      existence

      proof

        reconsider H1 = ( meet (( Carr U0) .: H)) as non empty Subset of U0 by Th12;

        ( UniAlgSetClosed H1) = UAStr (# H1, ( Opers (U0,H1)) #) by Th14, UNIALG_2:def 8;

        hence thesis;

      end;

      uniqueness by UNIALG_2: 12;

    end

    theorem :: UNIALG_3:15



     Th15: for U0 be with_const_op Universal_Algebra holds for l1,l2 be Element of ( UnSubAlLattice U0), U1,U2 be strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds l1 [= l2 iff the carrier of U1 c= the carrier of U2

    proof

      let U0 be with_const_op Universal_Algebra;

      let l1,l2 be Element of ( UnSubAlLattice U0);

      let U1,U2 be strict SubAlgebra of U0;

      reconsider l1 = U1 as Element of ( UnSubAlLattice U0) by UNIALG_2:def 14;

      reconsider l2 = U2 as Element of ( UnSubAlLattice U0) by UNIALG_2:def 14;



       A1: l1 [= l2 implies the carrier of U1 c= the carrier of U2

      proof

        reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;

        reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;

        reconsider U3 = (U11 \/ U21) as non empty Subset of U0;

        assume l1 [= l2;

        then (l1 "\/" l2) = l2;

        then (U1 "\/" U2) = U2 by UNIALG_2:def 15;

        then ( GenUnivAlg U3) = U2 by UNIALG_2:def 13;

        then

         A2: (the carrier of U1 \/ the carrier of U2) c= the carrier of U2 by UNIALG_2:def 12;

        the carrier of U2 c= (the carrier of U1 \/ the carrier of U2) by XBOOLE_1: 7;

        then (the carrier of U1 \/ the carrier of U2) = the carrier of U2 by A2;

        hence thesis by XBOOLE_1: 7;

      end;

      the carrier of U1 c= the carrier of U2 implies l1 [= l2

      proof

        reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;

        reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;

        reconsider U3 = (U11 \/ U21) as non empty Subset of U0;

        assume the carrier of U1 c= the carrier of U2;

        then ( GenUnivAlg U3) = U2 by UNIALG_2: 19, XBOOLE_1: 12;

        then (U1 "\/" U2) = U2 by UNIALG_2:def 13;

        then (l1 "\/" l2) = l2 by UNIALG_2:def 15;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: UNIALG_3:16

    for U0 be with_const_op Universal_Algebra holds for l1,l2 be Element of ( UnSubAlLattice U0), U1,U2 be strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds l1 [= l2 iff U1 is SubAlgebra of U2

    proof

      let U0 be with_const_op Universal_Algebra;

      let l1,l2 be Element of ( UnSubAlLattice U0);

      let U1,U2 be strict SubAlgebra of U0 such that

       A1: l1 = U1 & l2 = U2;

      thus l1 [= l2 implies U1 is SubAlgebra of U2

      proof

        assume l1 [= l2;

        then the carrier of U1 c= the carrier of U2 by A1, Th15;

        hence thesis by UNIALG_2: 11;

      end;

      thus U1 is SubAlgebra of U2 implies l1 [= l2

      proof

        assume U1 is SubAlgebra of U2;

        then the carrier of U1 is Subset of U2 by UNIALG_2:def 7;

        hence thesis by A1, Th15;

      end;

    end;

    theorem :: UNIALG_3:17



     Th17: for U0 be with_const_op strict Universal_Algebra holds ( UnSubAlLattice U0) is bounded

    proof

      let U0 be with_const_op strict Universal_Algebra;



       A1: ( UnSubAlLattice U0) is lower-bounded

      proof

        reconsider U11 = ( Constants U0) as Subset of U0;

        reconsider U2 = ( GenUnivAlg ( Constants U0)) as strict SubAlgebra of U0;

        reconsider l1 = ( GenUnivAlg ( Constants U0)) as Element of ( UnSubAlLattice U0) by UNIALG_2:def 14;

        take l1;

        let l2 be Element of ( UnSubAlLattice U0);

        reconsider U1 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;

        reconsider U21 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;

        reconsider U3 = (U11 \/ U21) as non empty Subset of U0;

        ( Constants U0) is Subset of U1 by UNIALG_2: 16;

        then ( GenUnivAlg U3) = U1 by UNIALG_2: 19, XBOOLE_1: 12;

        then (U2 "\/" U1) = U1 by UNIALG_2: 20;

        then (l1 "\/" l2) = l2 by UNIALG_2:def 15;

        then

         A2: l1 [= l2;

        hence (l1 "/\" l2) = l1 by LATTICES: 4;

        thus (l2 "/\" l1) = l1 by A2, LATTICES: 4;

      end;

      ( UnSubAlLattice U0) is upper-bounded

      proof

        U0 is strict SubAlgebra of U0 by UNIALG_2: 8;

        then

        reconsider l1 = U0 as Element of ( UnSubAlLattice U0) by UNIALG_2:def 14;

        reconsider U1 = l1 as strict SubAlgebra of U0 by UNIALG_2: 8;

        take l1;

        let l2 be Element of ( UnSubAlLattice U0);

        reconsider U2 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;

        reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;

        reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;

        reconsider H = (U11 \/ U21) as non empty Subset of U0;



         A3: H = the carrier of U1 by XBOOLE_1: 12;



        thus (l1 "\/" l2) = (U1 "\/" U2) by UNIALG_2:def 15

        .= ( GenUnivAlg ( [#] the carrier of U1)) by A3, UNIALG_2:def 13

        .= l1 by UNIALG_2: 18;

        hence (l2 "\/" l1) = l1;

      end;

      hence thesis by A1;

    end;

    registration

      let U0 be with_const_op strict Universal_Algebra;

      cluster ( UnSubAlLattice U0) -> bounded;

      coherence by Th17;

    end

    theorem :: UNIALG_3:18



     Th18: for U0 be with_const_op strict Universal_Algebra holds for U1 be strict SubAlgebra of U0 holds (( GenUnivAlg ( Constants U0)) /\ U1) = ( GenUnivAlg ( Constants U0))

    proof

      let U0 be with_const_op strict Universal_Algebra;

      let U1 be strict SubAlgebra of U0;

      set C = ( Constants U0), G = ( GenUnivAlg C);

      C is Subset of U1 by UNIALG_2: 15;

      then G is strict SubAlgebra of U1 by UNIALG_2:def 12;

      then

       A1: the carrier of G is Subset of U1 by UNIALG_2:def 7;

      the carrier of G meets the carrier of U1 by UNIALG_2: 17;

      then the carrier of (G /\ U1) = (the carrier of G /\ the carrier of U1) by UNIALG_2:def 9;

      hence thesis by A1, UNIALG_2: 12, XBOOLE_1: 28;

    end;

    theorem :: UNIALG_3:19

    for U0 be with_const_op strict Universal_Algebra holds ( Bottom ( UnSubAlLattice U0)) = ( GenUnivAlg ( Constants U0))

    proof

      let U0 be with_const_op strict Universal_Algebra;

      set L = ( UnSubAlLattice U0);

      set C = ( Constants U0);

      reconsider G = ( GenUnivAlg C) as Element of ( Sub U0) by UNIALG_2:def 14;

      reconsider l1 = G as Element of L;

      now

        let l be Element of L;

        reconsider u1 = l as Element of ( Sub U0);

        reconsider U2 = u1 as strict SubAlgebra of U0 by UNIALG_2:def 14;



        thus (l1 "/\" l) = (( GenUnivAlg C) /\ U2) by UNIALG_2:def 16

        .= l1 by Th18;

        hence (l "/\" l1) = l1;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: UNIALG_3:20



     Th20: for U0 be with_const_op strict Universal_Algebra holds for U1 be SubAlgebra of U0 holds for H be Subset of U0 st H = the carrier of U0 holds (( GenUnivAlg H) "\/" U1) = ( GenUnivAlg H)

    proof

      let U0 be with_const_op strict Universal_Algebra;

      let U1 be SubAlgebra of U0, H be Subset of U0;

      assume H = the carrier of U0;

      then (H \/ the carrier of U1) = H by Th3, XBOOLE_1: 12;

      hence thesis by UNIALG_2: 20;

    end;

    theorem :: UNIALG_3:21



     Th21: for U0 be with_const_op strict Universal_Algebra holds for H be Subset of U0 st H = the carrier of U0 holds ( Top ( UnSubAlLattice U0)) = ( GenUnivAlg H)

    proof

      let U0 be with_const_op strict Universal_Algebra;

      let H be Subset of U0;

      set L = ( UnSubAlLattice U0);

      reconsider u1 = ( GenUnivAlg H) as Element of ( Sub U0) by UNIALG_2:def 14;

      reconsider l1 = u1 as Element of L;

      assume

       A1: H = the carrier of U0;

      now

        let l be Element of L;

        reconsider u2 = l as Element of ( Sub U0);

        reconsider U2 = u2 as strict SubAlgebra of U0 by UNIALG_2:def 14;



        thus (l1 "\/" l) = (( GenUnivAlg H) "\/" U2) by UNIALG_2:def 15

        .= l1 by A1, Th20;

        hence (l "\/" l1) = l1;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: UNIALG_3:22

    for U0 be with_const_op strict Universal_Algebra holds ( Top ( UnSubAlLattice U0)) = U0

    proof

      let U0 be with_const_op strict Universal_Algebra;



       A1: U0 is strict SubAlgebra of U0 by UNIALG_2: 8;

      the carrier of U0 c= the carrier of U0;

      then

      reconsider H = the carrier of U0 as Subset of U0;



      thus ( Top ( UnSubAlLattice U0)) = ( GenUnivAlg H) by Th21

      .= U0 by A1, UNIALG_2: 19;

    end;

    theorem :: UNIALG_3:23

    for U0 be with_const_op strict Universal_Algebra holds ( UnSubAlLattice U0) is complete

    proof

      let U0 be with_const_op strict Universal_Algebra;

      let L be Subset of ( UnSubAlLattice U0);

      per cases ;

        suppose

         A1: L = {} ;

        thus thesis

        proof

          take ( Top ( UnSubAlLattice U0));

          thus ( Top ( UnSubAlLattice U0)) is_less_than L by A1;

          let l2 be Element of ( UnSubAlLattice U0);

          assume l2 is_less_than L;

          thus thesis by LATTICES: 19;

        end;

      end;

        suppose L <> {} ;

        then

        reconsider H = L as non empty Subset of ( Sub U0);

        reconsider l1 = ( meet H) as Element of ( UnSubAlLattice U0) by UNIALG_2:def 14;

        take l1;

        set x = the Element of H;

        thus l1 is_less_than L

        proof

          let l2 be Element of ( UnSubAlLattice U0);

          reconsider U1 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;

          reconsider u = l2 as Element of ( Sub U0);

          assume

           A2: l2 in L;

          (( Carr U0) . u) = the carrier of U1 by Def4;

          then ( meet (( Carr U0) .: H)) c= the carrier of U1 by A2, FUNCT_2: 35, SETFAM_1: 3;

          then the carrier of ( meet H) c= the carrier of U1 by Def5;

          hence l1 [= l2 by Th15;

        end;

        let l3 be Element of ( UnSubAlLattice U0);

        reconsider U1 = l3 as strict SubAlgebra of U0 by UNIALG_2:def 14;

        assume

         A3: l3 is_less_than L;



         A4: for A be set st A in (( Carr U0) .: H) holds the carrier of U1 c= A

        proof

          let A be set;

          assume

           A5: A in (( Carr U0) .: H);

          then

          reconsider H1 = A as Subset of U0;

          consider l4 be Element of ( Sub U0) such that

           A6: l4 in H & H1 = (( Carr U0) . l4) by A5, FUNCT_2: 65;

          reconsider l4 as Element of ( UnSubAlLattice U0);

          reconsider U2 = l4 as strict SubAlgebra of U0 by UNIALG_2:def 14;

          A = the carrier of U2 & l3 [= l4 by A3, A6, Def4;

          hence thesis by Th15;

        end;

        (( Carr U0) . x) in (( Carr U0) .: L) by FUNCT_2: 35;

        then the carrier of U1 c= ( meet (( Carr U0) .: H)) by A4, SETFAM_1: 5;

        then the carrier of U1 c= the carrier of ( meet H) by Def5;

        hence l3 [= l1 by Th15;

      end;

    end;

    definition

      let U01,U02 be with_const_op Universal_Algebra;

      let F be Function of the carrier of U01, the carrier of U02;

      :: UNIALG_3:def6

      func FuncLatt F -> Function of the carrier of ( UnSubAlLattice U01), the carrier of ( UnSubAlLattice U02) means

      : Def6: for U1 be strict SubAlgebra of U01, H be Subset of U02 st H = (F .: the carrier of U1) holds (it . U1) = ( GenUnivAlg H);

      existence

      proof

        defpred P[ object, object] means for U1 be strict SubAlgebra of U01 st U1 = $1 holds for S be Subset of U02 st S = (F .: the carrier of U1) holds $2 = ( GenUnivAlg (F .: the carrier of U1));



         A1: for u1 be object st u1 in the carrier of ( UnSubAlLattice U01) holds ex u2 be object st u2 in the carrier of ( UnSubAlLattice U02) & P[u1, u2]

        proof

          let u1 be object;

          assume u1 in the carrier of ( UnSubAlLattice U01);

          then

          consider U2 be strict SubAlgebra of U01 such that

           A2: U2 = u1 by Th1;

          reconsider u2 = ( GenUnivAlg (F .: the carrier of U2)) as strict SubAlgebra of U02;

          reconsider u2 as Element of ( UnSubAlLattice U02) by UNIALG_2:def 14;

          take u2;

          thus thesis by A2;

        end;

        consider f1 be Function of the carrier of ( UnSubAlLattice U01), the carrier of ( UnSubAlLattice U02) such that

         A3: for u1 be object st u1 in the carrier of ( UnSubAlLattice U01) holds P[u1, (f1 . u1)] from FUNCT_2:sch 1( A1);

        take f1;

        thus thesis

        proof

          let U1 be strict SubAlgebra of U01;

          let S be Subset of U02;



           A4: U1 is Element of ( Sub U01) by UNIALG_2:def 14;

          assume S = (F .: the carrier of U1);

          hence thesis by A3, A4;

        end;

      end;

      uniqueness

      proof

        let F1,F2 be Function of the carrier of ( UnSubAlLattice U01), the carrier of ( UnSubAlLattice U02) such that

         A5: for U1 be strict SubAlgebra of U01, H be Subset of U02 st H = (F .: the carrier of U1) holds (F1 . U1) = ( GenUnivAlg H) and

         A6: for U1 be strict SubAlgebra of U01, H be Subset of U02 st H = (F .: the carrier of U1) holds (F2 . U1) = ( GenUnivAlg H);

        for l be object st l in the carrier of ( UnSubAlLattice U01) holds (F1 . l) = (F2 . l)

        proof

          let l be object;

          assume l in the carrier of ( UnSubAlLattice U01);

          then

          consider U1 be strict SubAlgebra of U01 such that

           A7: U1 = l by Th1;

          consider H be Subset of U02 such that

           A8: H = (F .: the carrier of U1);

          (F1 . l) = ( GenUnivAlg H) by A5, A7, A8;

          hence thesis by A6, A7, A8;

        end;

        hence F1 = F2 by FUNCT_2: 12;

      end;

    end

    theorem :: UNIALG_3:24

    for U0 be with_const_op strict Universal_Algebra holds for F be Function of the carrier of U0, the carrier of U0 st F = ( id the carrier of U0) holds ( FuncLatt F) = ( id the carrier of ( UnSubAlLattice U0))

    proof

      let U0 be with_const_op strict Universal_Algebra;

      let F be Function of the carrier of U0, the carrier of U0 such that

       A1: F = ( id the carrier of U0);



       A2: for a be object st a in the carrier of ( UnSubAlLattice U0) holds (( FuncLatt F) . a) = a

      proof

        let a be object;

        assume a in the carrier of ( UnSubAlLattice U0);

        then

        reconsider a as strict SubAlgebra of U0 by UNIALG_2:def 14;

        for a1 be object holds a1 in the carrier of a implies a1 in (F .: the carrier of a)

        proof

          let a1 be object;

          assume

           A3: a1 in the carrier of a;

          the carrier of a c= the carrier of U0 by Th3;

          then

          reconsider a1 as Element of U0 by A3;

          (F . a1) = a1 by A1, FUNCT_1: 17;

          hence thesis by A3, FUNCT_2: 35;

        end;

        then

         A4: the carrier of a c= (F .: the carrier of a);

        for a1 be object holds a1 in (F .: the carrier of a) implies a1 in the carrier of a

        proof

          let a1 be object;

          assume

           A5: a1 in (F .: the carrier of a);

          then

          reconsider a1 as Element of U0;

          ex H be Element of U0 st H in the carrier of a & a1 = (F . H) by A5, FUNCT_2: 65;

          hence thesis by A1, FUNCT_1: 17;

        end;

        then

         A6: (F .: the carrier of a) c= the carrier of a;

        then

        reconsider H1 = the carrier of a as Subset of U0 by A4, XBOOLE_0:def 10;

        (F .: the carrier of a) = the carrier of a by A6, A4;

        then (( FuncLatt F) . a) = ( GenUnivAlg H1) by Def6;

        hence thesis by UNIALG_2: 19;

      end;

      ( dom ( FuncLatt F)) = the carrier of ( UnSubAlLattice U0) by FUNCT_2:def 1;

      hence thesis by A2, FUNCT_1: 17;

    end;