:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
::  by Ewa Burakowska
::
:: Received July 8, 1993
:: Copyright (c) 1993-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, TARSKI, UNIALG_1, FUNCT_2,
      PARTFUN1, RELAT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, CQC_SIM1, FUNCT_1,
      CARD_1, ZFMISC_1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, UNIALG_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
      STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, SETFAM_1, FUNCOP_1, PARTFUN1,
      FINSEQ_2, LATTICES, BINOP_1, UNIALG_1, MARGREL1;
 constructors SETFAM_1, BINOP_1, DOMAIN_1, FUNCOP_1, LATTICES, UNIALG_1,
      MARGREL1, FINSEQ_2, RELSET_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSEQ_2, STRUCT_0,
      LATTICES, UNIALG_1, ORDINAL1, FINSEQ_1, CARD_1, MARGREL1;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions TARSKI, XBOOLE_0, MARGREL1;
 equalities SUBSET_1, FUNCOP_1;
 expansions TARSKI, XBOOLE_0, MARGREL1;
 theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, UNIALG_1, ZFMISC_1,
      SETFAM_1, FUNCOP_1, BINOP_1, LATTICES, FINSEQ_3, RELAT_1, RELSET_1,
      XBOOLE_0, XBOOLE_1, MARGREL1;
 schemes FINSEQ_1, BINOP_1, XFAMILY;

begin

reserve U0,U1,U2,U3 for Universal_Algebra,
  n for Nat,
  x,y for set;

definition
  let U1;
  mode PFuncsDomHQN of U1 is PFuncsDomHQN of (the carrier of U1);
end;

definition
  let U1 be UAStr;
  mode PartFunc of U1 is PartFunc of (the carrier of U1)*,the carrier of U1;
end;

definition

  let U1,U2;
  pred U1,U2 are_similar means

  signature (U1) = signature (U2);
  symmetry;
  reflexivity;
end;

theorem
  U1,U2 are_similar implies len the charact of(U1) = len the charact of( U2)
proof
A1: len signature (U1) = len the charact of(U1) & len signature (U2) = len
  the charact of(U2) by UNIALG_1:def 4;
  assume U1,U2 are_similar;
  hence thesis by A1;
end;

theorem
  U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar;

theorem
  rng the charact of(U0) is non empty Subset of PFuncs((the carrier of
  U0)*,the carrier of U0) by FINSEQ_1:def 4,RELAT_1:41;

definition
  let U0;
  func Operations(U0) -> PFuncsDomHQN of U0 equals
  rng the charact of(U0);
  coherence
  proof
    reconsider A=rng the charact of(U0) as non empty set by RELAT_1:41;
    now
      let x be Element of A;
      consider i being Nat such that
A1:   i in dom(the charact of(U0)) and
A2:   (the charact of(U0)).i = x by FINSEQ_2:10;
      reconsider p = (the charact of U0).i as PartFunc of U0 by A1,UNIALG_1:1;
      p is homogeneous quasi_total non empty by A1,FUNCT_1:def 9
,MARGREL1:def 24;
      hence x is homogeneous quasi_total non empty PartFunc of U0 by A2;
    end;
    hence thesis by MARGREL1:def 26;
  end;
end;

definition
  let U1;
  mode operation of U1 is Element of Operations(U1);
end;

reserve A for non empty Subset of U0,
  o for operation of U0,
  x1,y1 for FinSequence of A;

definition
  let U0 be Universal_Algebra, A be Subset of U0, o be operation of U0;
  pred A is_closed_on o means

  for s being FinSequence of A st len s = arity o holds o.s in A;
end;

definition
  let U0 be Universal_Algebra, A be Subset of U0;
  attr A is opers_closed means

  for o be operation of U0 holds A is_closed_on o;
end;

definition
  let U0,A,o;
  assume
A1: A is_closed_on o;
  func o/.A ->homogeneous quasi_total non empty PartFunc of A*,A equals
  :Def5:
  o|((arity o)-tuples_on A);
  coherence
  proof
A2: (arity o)-tuples_on A c= (arity o)-tuples_on the carrier of U0
    proof
      let x be object;
      assume x in (arity o)-tuples_on A;
      then x in { s where s is Element of A* : len s =arity o} by
FINSEQ_2:def 4;
      then consider s be Element of A* such that
A3:   x = s and
A4:   len s = arity o;
      rng s c= A by FINSEQ_1:def 4;
      then rng s c= the carrier of U0 by XBOOLE_1:1;
      then reconsider s as FinSequence of the carrier of U0 by FINSEQ_1:def 4;
      reconsider s as Element of (the carrier of U0)* by FINSEQ_1:def 11;
      x=s by A3;
      then
      x in { s1 where s1 is Element of(the carrier of U0)*: len s1 =arity
      o} by A4;
      hence thesis by FINSEQ_2:def 4;
    end;
A5: dom ( o|((arity o)-tuples_on A))= (dom o) /\ ((arity o)-tuples_on A)
    by RELAT_1:61
      .=((arity o)-tuples_on the carrier of U0) /\ ((arity o)-tuples_on A)
    by MARGREL1:22
      .=(arity o)-tuples_on A by A2,XBOOLE_1:28;
A6: rng (o|((arity o)-tuples_on A)) c= A
    proof
      let x be object;
      assume x in rng( o|((arity o)-tuples_on A));
      then consider y being object such that
A7:   y in dom ( o|((arity o)-tuples_on A)) and
A8:   x = (o|((arity o)-tuples_on A)).y by FUNCT_1:def 3;
      y in { s where s is Element of A* : len s =arity o} by A5,A7,
FINSEQ_2:def 4;
      then consider s be Element of A* such that
A9:   y = s and
A10:  len s = arity o;
      (o|((arity o)-tuples_on A)).s = o.s by A7,A9,FUNCT_1:47;
      hence thesis by A1,A8,A9,A10;
    end;
    (arity o)-tuples_on A in the set of all i-tuples_on A where i is Nat;
    then (arity o)-tuples_on A c=
     union the set of all i-tuples_on A where i is Nat by ZFMISC_1:74;
    then dom ( o|((arity o)-tuples_on A)) c= A* by A5,FINSEQ_2:108;
    then reconsider oa = o|((arity o)-tuples_on A) as PartFunc of A*,A by A6,
RELSET_1:4;
A11: oa is homogeneous
    proof
      let x1,y1 be FinSequence;
      assume that
A12:  x1 in dom oa and
A13:  y1 in dom oa;
      y1 in { s1 where s1 is Element of A* : len s1=arity o} by A5,A13,
FINSEQ_2:def 4;
      then
A14:  ex s1 be Element of A* st y1=s1 & len s1 = arity o;
      x1 in { s where s is Element of A* : len s =arity o} by A5,A12,
FINSEQ_2:def 4;
      then ex s be Element of A* st x1 = s & len s = arity o;
      hence thesis by A14;
    end;
    oa is quasi_total
    proof
      let x1,y1;
      assume that
A15:  len x1 = len y1 and
A16:  x1 in dom oa;
      x1 in { s where s is Element of A* : len s =arity o} by A5,A16,
FINSEQ_2:def 4;
      then ex s be Element of A* st x1 = s & len s = arity o;
      then y1 is Element of (arity o)-tuples_on A by A15,FINSEQ_2:92;
      hence thesis by A5;
    end;
    hence thesis by A5,A11;
  end;
end;

definition
  let U0,A;
  func Opers(U0,A) -> PFuncFinSequence of A means
  :Def6:
  dom it = dom the
  charact of(U0) & for n being set,o st n in dom it & o =(the charact of(U0)).n
  holds it.n = o/.A;
  existence
  proof
    defpred P[Nat,set] means for o st o =(the charact of(U0)).$1 holds $2 = o
    /.A;
A1: for n being Nat st n in Seg len the charact of(U0) ex x being Element
    of PFuncs(A*,A) st P[n,x]
    proof
      let n be Nat;
      assume n in Seg len the charact of(U0);
      then n in dom the charact of(U0) by FINSEQ_1:def 3;
      then reconsider o1 =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
      reconsider x = o1/.A as Element of PFuncs(A*,A) by PARTFUN1:45;
      take x;
      let o;
      assume o = (the charact of(U0)).n;
      hence thesis;
    end;
    consider p being FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len the charact of(U0) and
A3: for n being Nat st n in Seg len the charact of(U0) holds P[n,p.n]
    from FINSEQ_1:sch 5(A1);
    reconsider p as PFuncFinSequence of A;
    take p;
    thus dom p =dom the charact of(U0) by A2,FINSEQ_1:def 3;
    let n be set,o;
    assume n in dom p & o =(the charact of(U0)).n;
    hence thesis by A2,A3;
  end;
  uniqueness
  proof
    let p1,p2 be PFuncFinSequence of A;
    assume that
A4: dom p1 = dom the charact of(U0) and
A5: for n being set,o st n in dom p1 & o = (the charact of(U0)).n
    holds p1.n = o/.A and
A6: dom p2 = dom the charact of(U0) and
A7: for n being set,o st n in dom p2 & o = (the charact of(U0)).n
    holds p2.n = o/.A;
    for n be Nat st n in dom the charact of(U0) holds p1.n = p2.n
    proof
      let n be Nat;
      assume
A8:   n in dom the charact of(U0);
      then reconsider k =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
      p1.n =k/.A by A4,A5,A8;
      hence thesis by A6,A7,A8;
    end;
    hence thesis by A4,A6,FINSEQ_1:13;
  end;
end;

theorem Th4:
  for B being non empty Subset of U0 st B=the carrier of U0 holds B
  is opers_closed & for o holds o/.B = o
proof
  let B be non empty Subset of U0;
  assume
A1: B=the carrier of U0;
A2: for o holds B is_closed_on o
  proof
    let o;
    let s be FinSequence of B;
    assume
A3: len s = arity o;
    dom o = (arity o)-tuples_on B & s is Element of (len s)-tuples_on B by A1,
FINSEQ_2:92,MARGREL1:22;
    then
A4: o.s in rng o by A3,FUNCT_1:def 3;
    rng o c= B by A1,RELAT_1:def 19;
    hence thesis by A4;
  end;
  for o holds o/.B = o
  proof
    let o;
    dom o = (arity(o))-tuples_on B & o/.B =o|((arity(o))-tuples_on B) by A1,A2
,Def5,MARGREL1:22;
    hence thesis by RELAT_1:68;
  end;
  hence thesis by A2;
end;

theorem
  for U1 be Universal_Algebra, A be non empty Subset of U1, o be
  operation of U1 st A is_closed_on o holds arity (o/.A) = arity o
proof
  let U1 be Universal_Algebra, A be non empty Subset of U1, o be operation of
  U1;
  assume A is_closed_on o;
  then o/.A =o|((arity o)-tuples_on A) by Def5;
  then dom (o/.A) = dom o /\ ((arity o)-tuples_on A) by RELAT_1:61;
  then
A1: dom (o/.A) = ((arity o)-tuples_on the carrier of U1) /\ ((arity o)
  -tuples_on A) by MARGREL1:22
    .= (arity o)-tuples_on A by MARGREL1:21;
  dom (o/.A)=(arity (o/.A))-tuples_on A by MARGREL1:22;
  hence thesis by A1,FINSEQ_2:110;
end;

definition
  let U0;
  mode SubAlgebra of U0 -> Universal_Algebra means
    :Def7:
    the carrier of it is
Subset of U0 & for B be non empty Subset of U0 st B=the carrier of it holds the
    charact of it = Opers(U0,B) & B is opers_closed;
  existence
  proof
    take U1=U0;
A1: for B be non empty Subset of U0 st B=the carrier of U0 holds the
    charact of(U0) = Opers(U0,B) & B is opers_closed
    proof
      let B be non empty Subset of U0;
      assume
A2:   B =the carrier of U0;
A3:   dom the charact of(U0) = dom Opers(U0,B) by Def6;
      for n be Nat st n in dom the charact of(U0) holds (the charact of(U0
      )).n = (Opers(U0,B)).n
      proof
        let n be Nat;
        assume
A4:     n in dom the charact of(U0);
        then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
        (Opers(U0,B)).n = o/.B by A3,A4,Def6;
        hence thesis by A2,Th4;
      end;
      hence thesis by A2,A3,Th4,FINSEQ_1:13;
    end;
    the carrier of U1 c= the carrier of U1;
    hence thesis by A1;
  end;
end;

registration
  let U0 be Universal_Algebra;
  cluster strict for SubAlgebra of U0;
  existence
  proof
    reconsider S = UAStr(#the carrier of U0,the charact of U0#) as strict
    Universal_Algebra by UNIALG_1:def 1,def 2,def 3;
A1: the carrier of S c= the carrier of U0;
    for B be non empty Subset of U0 st B=the carrier of S holds the
    charact of(S) = Opers(U0,B) & B is opers_closed
    proof
      let B be non empty Subset of U0;
      assume
A2:   B=the carrier of S;
A3:   now
        let n be Nat;
        assume
A4:     n in dom the charact of (U0);
        then reconsider o = (the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
        n in dom Opers(U0,B) by A4,Def6;
        hence Opers (U0,B).n = o/.B by Def6
          .= (the charact of(U0)).n by A2,Th4;
      end;
      dom the charact of(U0)= dom Opers(U0,B) by Def6;
      hence thesis by A2,A3,Th4,FINSEQ_1:13;
    end;
    then reconsider S as SubAlgebra of U0 by A1,Def7;
    take S;
    thus thesis;
  end;
end;

theorem Th6:
  for U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be
operation of U1, n be Nat st U0 is SubAlgebra of U1 & n in dom the charact of(
U0) & o0 = (the charact of(U0)).n & o1 = (the charact of(U1)).n holds arity o0
  = arity o1
proof
  let U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1
  ,n;
  assume that
A1: U0 is SubAlgebra of U1 and
A2: n in dom the charact of(U0) & o0 = (the charact of(U0)).n and
A3: o1 = (the charact of(U1)).n;
  reconsider A =the carrier of U0 as non empty Subset of U1 by A1,Def7;
  A is opers_closed by A1,Def7;
  then
A4: A is_closed_on o1;
  n in dom Opers(U1,A) & o0 = Opers(U1,A).n by A1,A2,Def7;
  then o0 = o1/.A by A3,Def6;
  then o0 = o1|((arity o1)-tuples_on A) by A4,Def5;
  then dom o0 = dom o1 /\ ((arity o1)-tuples_on A) by RELAT_1:61;
  then
A5: dom o0 = ((arity o1)-tuples_on the carrier of U1) /\ ((arity o1)
  -tuples_on A) by MARGREL1:22
    .= (arity o1)-tuples_on A by MARGREL1:21;
  dom o0 =(arity o0)-tuples_on A by MARGREL1:22;
  hence thesis by A5,FINSEQ_2:110;
end;

theorem Th7:
  U0 is SubAlgebra of U1 implies dom the charact of(U0)=dom the charact of(U1)
proof
  assume
A1: U0 is SubAlgebra of U1;
  then reconsider A =the carrier of U0 as non empty Subset of U1 by Def7;
  the charact of(U0) = Opers(U1,A) by A1,Def7;
  hence thesis by Def6;
end;

theorem
  U0 is SubAlgebra of U0
proof
A1: for B be non empty Subset of U0 st B=the carrier of U0 holds the charact
  of(U0) = Opers(U0,B) & B is opers_closed
  proof
    let B be non empty Subset of U0;
    assume
A2: B =the carrier of U0;
A3: dom the charact of(U0) = dom Opers(U0,B) by Def6;
    for n be Nat st n in dom the charact of(U0) holds (the charact of(U0))
    .n = (Opers(U0,B)).n
    proof
      let n be Nat;
      assume
A4:   n in dom the charact of(U0);
      then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
      (Opers(U0,B)).n = o/.B by A3,A4,Def6;
      hence thesis by A2,Th4;
    end;
    hence thesis by A2,A3,Th4,FINSEQ_1:13;
  end;
  the carrier of U0 c= the carrier of U0;
  hence thesis by A1,Def7;
end;

theorem
  U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is
  SubAlgebra of U2
proof
  assume that
A1: U0 is SubAlgebra of U1 and
A2: U1 is SubAlgebra of U2;
A3: the carrier of U0 is Subset of U1 by A1,Def7;
  reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2,Def7;
A4: the charact of(U1) = Opers(U2,B2) by A2,Def7;
  the carrier of U1 is Subset of U2 by A2,Def7;
  hence the carrier of U0 is Subset of U2 by A3,XBOOLE_1:1;
  let B be non empty Subset of U2;
  assume
A5: B = the carrier of U0;
  reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1,Def7;
A6: the charact of(U0) = Opers(U1,B1) by A1,Def7;
A7: B2 is opers_closed by A2,Def7;
A8: dom the charact of(U1)= dom Opers(U2,B2) by A2,Def7
    .= dom the charact of(U2) by Def6;
A9: B1 is opers_closed by A1,Def7;
A10: now
    let o2 be operation of U2;
    consider n being Nat such that
A11: n in dom the charact of(U2) and
A12: (the charact of(U2)).n = o2 by FINSEQ_2:10;
A13: dom the charact of(U2) = dom Opers(U2,B2) by Def6;
    then reconsider o21 = (the charact of(U1)).n as operation of U1 by A4,A11,
FUNCT_1:def 3;
A14: dom o21 = (arity o21)-tuples_on (the carrier of U1) by MARGREL1:22;
A15: dom the charact of(U1) = dom Opers(U1,B1) by Def6;
    then reconsider
    o20 = (the charact of(U0)).n as operation of U0 by A6,A4,A11,A13,
FUNCT_1:def 3;
A16: dom o20 = (arity o20)-tuples_on (the carrier of U0) by MARGREL1:22;
A17: dom o2 = (arity o2)-tuples_on (the carrier of U2) & dom(o2 | ((arity
o2) -tuples_on B2)) = dom o2 /\ ((arity o2)-tuples_on B2)
 by MARGREL1:22,RELAT_1:61;
A18: B2 is_closed_on o2 by A7;
A19: o21 = o2/.B2 by A4,A11,A12,A13,Def6;
    then o21 = o2 | ((arity o2)-tuples_on B2) by A18,Def5;
    then
A20: arity o2 = arity o21 by A14,A17,FINSEQ_2:110,MARGREL1:21;
A21: B1 is_closed_on o21 by A9;
A22: o20 = o21 /. B1 by A6,A4,A11,A13,A15,Def6;
    then o20 = o21 | ((arity o21)-tuples_on B1) by A21,Def5;
    then (arity o20)-tuples_on B1 = (arity o21)-tuples_on (the carrier of U1)
    /\ (arity o21)-tuples_on B1 by A16,A14,RELAT_1:61;
    then
A23: arity o20 = arity o21 by FINSEQ_2:110,MARGREL1:21;
    now
      let s be FinSequence of B;
      reconsider s1 = s as Element of B1* by A5,FINSEQ_1:def 11;
      reconsider s0 = s as Element of (the carrier of U0)* by A5,
FINSEQ_1:def 11;
A24:  rng o20 c= B by A5,RELAT_1:def 19;
      rng s c= B by FINSEQ_1:def 4;
      then rng s c= B2 by A3,A5,XBOOLE_1:1;
      then s is FinSequence of B2 by FINSEQ_1:def 4;
      then reconsider s2 = s as Element of B2* by FINSEQ_1:def 11;
      assume
A25:  len s = arity o2;
      then s2 in {w where w is Element of B2*: len w = arity o2};
      then
A26:  s2 in (arity o2)-tuples_on B2 by FINSEQ_2:def 4;
      s0 in {w where w is Element of (the carrier of U0)*: len w = arity
      o20 } by A23,A20,A25;
      then s0 in (arity o20)-tuples_on (the carrier of U0) by FINSEQ_2:def 4;
      then
A27:  o20.s0 in rng o20 by A16,FUNCT_1:def 3;
      s1 in {w where w is Element of B1*: len w = arity o21} by A20,A25;
      then
A28:  s1 in (arity o21)-tuples_on B1 by FINSEQ_2:def 4;
      o20.s0 = (o21 | (arity o21)-tuples_on B1).s1 by A21,A22,Def5
        .= o21.s1 by A28,FUNCT_1:49
        .= (o2 | (arity o2)-tuples_on B2).s2 by A18,A19,Def5
        .= o2.s by A26,FUNCT_1:49;
      hence o2.s in B by A27,A24;
    end;
    hence B is_closed_on o2;
  end;
A29: dom the charact of(U0) = dom Opers(U1,B1) by A1,Def7
    .= dom the charact of(U1) by Def6;
A30: dom the charact of(U2)= dom Opers(U2,B) by Def6;
A31: B = B1 by A5;
  now
    let n be Nat;
    assume
A32: n in dom Opers(U2,B);
    then reconsider o2 = (the charact of(U2)).n as operation of U2 by A30,
FUNCT_1:def 3;
    reconsider o21 = (the charact of(U1)).n as operation of U1 by A8,A30,A32,
FUNCT_1:def 3;
A33: B2 is_closed_on o2 by A7;
A34: B1 is_closed_on o21 by A9;
    thus Opers(U2,B).n = o2/.B by A32,Def6
      .=o2|((arity o2)-tuples_on B) by A10,Def5
      .=o2|((arity o2)-tuples_on B2 /\ (arity o2)-tuples_on B)
       by A31,MARGREL1:21
      .=(o2|((arity o2)-tuples_on B2))|((arity o2)-tuples_on B)by RELAT_1:71
      .=(o2/.B2)|((arity o2)-tuples_on B) by A33,Def5
      .=o21|((arity o2)-tuples_on B) by A4,A8,A30,A32,Def6
      .=o21|((arity o21)-tuples_on B1) by A2,A5,A8,A30,A32,Th6
      .=o21/.B1 by A34,Def5
      .= (the charact of(U0)).n by A6,A29,A8,A30,A32,Def6;
  end;
  hence the charact of(U0) = Opers(U2,B) by A29,A8,A30,FINSEQ_1:13;
  thus thesis by A10;
end;

theorem Th10:
  U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2
proof
  assume that
A1: U1 is strict SubAlgebra of U2 and
A2: U2 is strict SubAlgebra of U1;
  reconsider B = the carrier of U1 as non empty Subset of U2 by A1,Def7;
  the carrier of U2 c= the carrier of U2;
  then reconsider B1 = the carrier of U2 as non empty Subset of U2;
A3: dom Opers(U2,B1) = dom the charact of (U2) by Def6;
A4: for n being Nat st n in dom the charact of(U2) holds (the charact of(U2)
  ).n = (Opers(U2,B1)).n
  proof
    let n be Nat;
    assume
A5: n in dom the charact of(U2);
    then reconsider o =(the charact of(U2)).n as operation of U2 by
FUNCT_1:def 3;
    (Opers(U2,B1)).n = o/.B1 by A3,A5,Def6
      .= o by Th4;
    hence thesis;
  end;
  the carrier of U2 is Subset of U1 by A2,Def7;
  then
A6: B1 = B;
  then the charact of(U1) = Opers(U2,B1) by A1,Def7;
  hence thesis by A1,A2,A6,A3,A4,FINSEQ_1:13;
end;

theorem Th11:
  for U1,U2 be SubAlgebra of U0 st the carrier of U1 c= the
  carrier of U2 holds U1 is SubAlgebra of U2
proof
  let U1,U2 be SubAlgebra of U0;
A1: dom the charact of(U1) = dom the charact of(U0) by Th7;
  reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;
  assume
A2: the carrier of U1 c= the carrier of U2;
  hence the carrier of U1 is Subset of U2;
  let B be non empty Subset of U2;
  assume
A3: B = the carrier of U1;
  reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;
A4: the charact of(U2) = Opers(U0,B2) by Def7;
A5: B2 is opers_closed by Def7;
A6: dom Opers(U2,B) = dom the charact of(U2) by Def6;
A7: dom the charact of(U2)= dom the charact of(U0) by Th7;
A8: B1 is opers_closed by Def7;
A9: B is opers_closed
  proof
    let o2 be operation of U2;
    let s be FinSequence of B;
    consider n being Nat such that
A10: n in dom the charact of(U2) and
A11: (the charact of(U2)).n = o2 by FINSEQ_2:10;
    reconsider o0 = (the charact of(U0)).n as operation of U0 by A7,A10,
FUNCT_1:def 3;
A12: arity o2 = arity o0 by A10,A11,Th6;
    rng s c= B by FINSEQ_1:def 4;
    then
 rng s c= B2 by XBOOLE_1:1;
    then s is FinSequence of B2 by FINSEQ_1:def 4;
    then reconsider s2 = s as Element of B2* by FINSEQ_1:def 11;
    reconsider s1 = s as Element of B1* by A3,FINSEQ_1:def 11;
    assume
A13: arity o2 = len s;
    set tb2 = (arity o0)-tuples_on B2;
A14: B2 is_closed_on o0 by A5;
A15: o2 = o0/.B2 by A4,A10,A11,Def6
      .= o0 | tb2 by A14,Def5;
A16: B1 is_closed_on o0 by A8;
    tb2 = {w where w is Element of B2*: len w = arity o0} by FINSEQ_2:def 4;
    then s2 in tb2 by A13,A12;
    then o2.s = o0.s1 by A15,FUNCT_1:49;
    hence thesis by A3,A13,A16,A12;
  end;
A17: the charact of(U1) = Opers(U0,B1) by Def7;
  now
    let n be Nat;
    assume
A18: n in dom the charact of(U0);
    then reconsider o0 = (the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
    reconsider o2 = (the charact of(U2)).n as operation of U2 by A7,A18,
FUNCT_1:def 3;
A19: o2 = o0/.B2 & arity o2 = arity o0 by A4,A7,A18,Def6,Th6;
A20: B is_closed_on o2 by A9;
A21: B2 is_closed_on o0 by A5;
A22: B1 is_closed_on o0 by A8;
    thus (the charact of(U1)).n = o0/.B1 by A17,A1,A18,Def6
      .= o0 | (arity o0)-tuples_on B1 by A22,Def5
      .= o0 | (((arity o0)-tuples_on B2) /\ ((arity o0)-tuples_on B1)) by A2,
MARGREL1:21
      .= (o0 | (arity o0)-tuples_on B2) | ((arity o0)-tuples_on B) by A3,
RELAT_1:71
      .= (o0 /. B2) | ((arity o0)-tuples_on B) by A21,Def5
      .= o2 /. B by A20,A19,Def5
      .= Opers(U2,B).n by A7,A6,A18,Def6;
  end;
  hence the charact of(U1) = Opers(U2,B) by A1,A7,A6,FINSEQ_1:13;
  thus thesis by A9;
end;

theorem Th12:
  for U1,U2 be strict SubAlgebra of U0 st the carrier of U1 = the
  carrier of U2 holds U1 = U2
proof
  let U1,U2 be strict SubAlgebra of U0;
  assume the carrier of U1 = the carrier of U2;
  then U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 by Th11;
  hence thesis by Th10;
end;

theorem
  U1 is SubAlgebra of U2 implies U1,U2 are_similar
proof
  set s1 = signature(U1), s2 = signature(U2);
  set X = dom s1;
  len s1 = len the charact of(U1) by UNIALG_1:def 4;
  then
A1: dom s1 = dom the charact of(U1) by FINSEQ_3:29;
  assume
A2: U1 is SubAlgebra of U2;
  then reconsider A = the carrier of U1 as non empty Subset of U2 by Def7;
  len s2 = len the charact of(U2) by UNIALG_1:def 4;
  then
A3: dom s2 = dom the charact of(U2) by FINSEQ_3:29;
  dom the charact of (U1)= dom Opers(U2,A) by A2,Def7;
  then
A4: dom s1 = dom s2 by A1,A3,Def6;
  the charact of(U1)=Opers(U2,A) by A2,Def7;
  then
A5: dom s1 c= dom s2 by A1,A3,Def6;
  for n being Nat st n in X holds s1.n = s2.n
  proof
    let n be Nat;
    assume
A6: n in X;
    then reconsider o1=(the charact of(U1)).n as operation of U1 by A1,
FUNCT_1:def 3;
    reconsider o2=(the charact of U2).n as operation of U2 by A3,A4,A6,
FUNCT_1:def 3;
    s1.n = arity(o1) & s2.n = arity(o2) by A5,A6,UNIALG_1:def 4;
    hence thesis by A2,A1,A6,Th6;
  end;
  then s1 = s2 by A4,FINSEQ_1:13;
  hence thesis;
end;

theorem Th14:
  for A be non empty Subset of U0 holds UAStr (#A,Opers(U0,A)#) is
  strict Universal_Algebra
proof
  let A be non empty Subset of U0;
  set C = UAStr(#A,Opers(U0,A)#);
A1: dom the charact of(C) = dom the charact of(U0) by Def6;
  for n be object st n in dom the charact of(C) holds (the charact of C).n
  is non empty
  proof
    let n be object;
    assume
A2: n in dom the charact of(C);
    then reconsider o = (the charact of U0).n as operation of U0 by A1,
FUNCT_1:def 3;
    (the charact of C).n =o/.A by A2,Def6;
    hence thesis;
  end;
  then
A3: the charact of(C) is non-empty by FUNCT_1:def 9;
  for n be Nat ,h be PartFunc of C st n in dom the charact of(C) & h = (
  the charact of C).n holds h is quasi_total
  proof
    let n;
    let h be PartFunc of (the carrier of C)*,the carrier of C;
    assume that
A4: n in dom the charact of(C) and
A5: h = (the charact of C).n;
    reconsider o = (the charact of U0).n as operation of U0 by A1,A4,
FUNCT_1:def 3;
    h =o/.A by A4,A5,Def6;
    hence thesis;
  end;
  then
A6: the charact of C is quasi_total;
  for n be Nat ,h be PartFunc of (the carrier of C)*,the carrier of C st n
  in dom the charact of(C) & h = (the charact of C).n holds h is homogeneous
  proof
    let n;
    let h be PartFunc of (the carrier of C)*,the carrier of C;
    assume that
A7: n in dom the charact of(C) and
A8: h = (the charact of C).n;
    reconsider o = (the charact of U0).n as operation of U0 by A1,A7,
FUNCT_1:def 3;
    h =o/.A by A7,A8,Def6;
    hence thesis;
  end;
  then
A9: the charact of (C) is homogeneous;
  the charact of C <> {} by A1,RELAT_1:38,41;
  hence thesis by A9,A6,A3,UNIALG_1:def 1,def 2,def 3;
end;

definition
  let U0 be Universal_Algebra, A be non empty Subset of U0;
  assume
A1: A is opers_closed;
  func UniAlgSetClosed(A) -> strict SubAlgebra of U0 equals
  :Def8:
  UAStr (# A,
    Opers(U0,A) #);
  coherence
  proof
    reconsider C = UAStr(# A,Opers(U0,A) #) as strict Universal_Algebra by Th14
;
    for B be non empty Subset of U0 st B =the carrier of C holds the
    charact of(C) = Opers(U0,B) & B is opers_closed by A1;
    hence thesis by Def7;
  end;
end;

definition
  let U0;
  let U1,U2 be SubAlgebra of U0;
  assume
A1: the carrier of U1 meets the carrier of U2;
  func U1 /\ U2 -> strict SubAlgebra of U0 means
  :Def9:
  the carrier of it = (
the carrier of U1) /\ (the carrier of U2) & for B be non empty Subset of U0 st
B=the carrier of it holds the charact of(it) = Opers(U0,B) & B is opers_closed;
  existence
  proof
A2: (the carrier of U1) /\ (the carrier of U2)c= the carrier of U1 by
XBOOLE_1:17;
    the carrier of U1 is Subset of U0 by Def7;
    then reconsider C =(the carrier of U1) /\ (the carrier of U2) as non empty
    Subset of U0 by A1,A2,XBOOLE_1:1;
    set S =UAStr(#C,Opers(U0,C)#);
A3: (the carrier of U1) /\ (the carrier of U2)c= the carrier of U2 by
XBOOLE_1:17;
A4: now
      let o be operation of U0;
      now
        set B1 =the carrier of U1, B2 =the carrier of U2;
        let s be FinSequence of C;
        reconsider s2=s as FinSequence of B2 by A3,FINSEQ_2:24;
        reconsider s1=s as FinSequence of B1 by A2,FINSEQ_2:24;
        assume
A5:     len s =arity o;
        reconsider B1 as non empty Subset of U0 by Def7;
        reconsider B2 as non empty Subset of U0 by Def7;
        B2 is opers_closed by Def7;
        then B2 is_closed_on o;
        then
A6:     o.s2 in B2 by A5;
        B1 is opers_closed by Def7;
        then B1 is_closed_on o;
        then o.s1 in B1 by A5;
        hence o.s in C by A6,XBOOLE_0:def 4;
      end;
      hence C is_closed_on o;
    end;
    then
A7: for B be non empty Subset of U0 st B=the carrier of S holds the
    charact of(S) = Opers(U0,B) & B is opers_closed;
    reconsider S as Universal_Algebra by Th14;
    reconsider S as strict SubAlgebra of U0 by A7,Def7;
    take S;
    thus thesis by A4;
  end;
  uniqueness
  proof
    the carrier of U1 is Subset of U0 & (the carrier of U1) /\ (the
    carrier of U2)c=(the carrier of U1) by Def7,XBOOLE_1:17;
    then reconsider C =(the carrier of U1) /\ (the carrier of U2) as non empty
    Subset of U0 by A1,XBOOLE_1:1;
    let W1,W2 be strict SubAlgebra of U0;
    assume that
A8: the carrier of W1 = (the carrier of U1) /\ (the carrier of U2) &
for B1 be non empty Subset of U0 st B1=the carrier of W1 holds the charact of(
    W1) = Opers (U0,B1) & B1 is opers_closed and
A9: the carrier of W2= (the carrier of U1) /\ (the carrier of U2) and
A10: for B2 be non empty Subset of U0 st B2=the carrier of W2 holds
    the charact of(W2) = Opers(U0,B2) & B2 is opers_closed;
    the charact of W2 = Opers(U0,C) by A9,A10;
    hence thesis by A8,A9;
  end;
end;

definition
  let U0;
  func Constants(U0) -> Subset of U0 equals
  { a where a is Element of U0: ex o
  be operation of U0 st arity o=0 & a in rng o};
  coherence
  proof
    set E = {a where a is Element of U0 : ex o be operation of U0 st arity o=0
    & a in rng o};
    E c= the carrier of U0
    proof
      let x be object;
      assume x in E;
      then
      ex w be Element of U0 st w=x & ex o be operation of U0 st arity o=0 &
      w in rng o;
      hence thesis;
    end;
    hence thesis;
  end;
end;

definition
  let IT be Universal_Algebra;
  attr IT is with_const_op means
  :Def11:
  ex o being operation of IT st arity o =0;
end;

registration
  cluster with_const_op strict for Universal_Algebra;
  existence
  proof
    set A = the non empty set;
    set a = the Element of A;
    reconsider w = <*>A .--> a as Element of PFuncs(A*,A) by MARGREL1:19;
    set U0 = UAStr (# A, <*w*> #);
A1: the charact of U0 is quasi_total & the charact of U0 is homogeneous by
MARGREL1:20;
    the charact of U0 is non-empty by MARGREL1:20;
    then reconsider U0 as Universal_Algebra by A1,UNIALG_1:def 1,def 2,def 3;
    take U0;
    dom <*w*> ={1} & 1 in {1} by FINSEQ_1:2,38,TARSKI:def 1;
    then reconsider o= (the charact of U0).1 as operation of U0 by
FUNCT_1:def 3;
    o=w by FINSEQ_1:40;
    then
A2: dom o = {<*>A} by FUNCOP_1:13;
A3: now
      let x be FinSequence;
      assume x in dom o;
      then x = <*>A by A2,TARSKI:def 1;
      hence len x = 0;
    end;
    <*>A in {<*>A} by TARSKI:def 1;
    then arity o = 0 by A2,A3,MARGREL1:def 25;
    hence thesis;
  end;
end;

registration
  let U0 be with_const_op Universal_Algebra;
  cluster Constants(U0) -> non empty;
  coherence
  proof
    consider o being operation of U0 such that
A1: arity o=0 by Def11;
    dom o = 0-tuples_on the carrier of U0 by A1,MARGREL1:22
      .={<*>the carrier of U0} by FINSEQ_2:94;
    then <*>the carrier of U0 in dom o by TARSKI:def 1;
    then
A2: o.(<*>the carrier of U0) in rng o by FUNCT_1:def 3;
    rng o c= the carrier of U0 by RELAT_1:def 19;
    then reconsider u = o.(<*>the carrier of U0) as Element of U0 by A2;
    u in { a where a is Element of U0: ex o be operation of U0 st arity o=
    0 & a in rng o} by A1,A2;
    hence thesis;
  end;
end;

theorem Th15:
  for U0 be Universal_Algebra, U1 be SubAlgebra of U0 holds
  Constants(U0) is Subset of U1
proof
  let U0 be Universal_Algebra, U1 be SubAlgebra of U0;
  set u1 = the carrier of U1;
  Constants(U0) c= u1
  proof
    reconsider B =u1 as non empty Subset of U0 by Def7;
    let x be object;
    assume x in Constants(U0);
    then consider a be Element of U0 such that
A1: a=x and
A2: ex o be operation of U0 st arity o=0 & a in rng o;
    consider o0 be operation of U0 such that
A3: arity o0 = 0 and
A4: a in rng o0 by A2;
    consider y be object such that
A5: y in dom o0 and
A6: a = o0.y by A4,FUNCT_1:def 3;
    dom o0 = 0-tuples_on the carrier of U0 by A3,MARGREL1:22
      .= {<*>the carrier of U0} by FINSEQ_2:94;
    then y in {<*>B} by A5;
    then y in 0-tuples_on B by FINSEQ_2:94;
    then y in dom o0 /\ (arity o0)-tuples_on B by A3,A5,XBOOLE_0:def 4;
    then
A7: y in dom (o0 | (arity o0)-tuples_on B) by RELAT_1:61;
    consider n being Nat such that
A8: n in dom (the charact of U0) and
A9: (the charact of U0).n=o0 by FINSEQ_2:10;
A10: n in dom the charact of(U1) by A8,Th7;
    then reconsider o1= (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
    the charact of(U1) =Opers(U0,B) by Def7;
    then
A11: o1=o0/.B by A9,A10,Def6;
    B is opers_closed by Def7;
    then
A12: B is_closed_on o0;
    then y in dom (o0/.B) by A7,Def5;
    then
A13: o1.y in rng o1 by A11,FUNCT_1:def 3;
A14: rng o1 c= the carrier of U1 by RELAT_1:def 19;
    o1.y = (o0 | (arity o0)-tuples_on B).y by A11,A12,Def5
      .= a by A6,A7,FUNCT_1:47;
    hence thesis by A1,A13,A14;
  end;
  hence thesis;
end;

theorem
  for U0 be with_const_op Universal_Algebra, U1 be SubAlgebra of U0
  holds Constants(U0) is non empty Subset of U1 by Th15;

theorem Th17:
  for U0 be with_const_op Universal_Algebra,U1,U2 be SubAlgebra of
  U0 holds the carrier of U1 meets the carrier of U2
proof
  let U0 be with_const_op Universal_Algebra, U1,U2 be SubAlgebra of U0;
  set a = the Element of Constants(U0);
  Constants(U0) is non empty Subset of U1 & Constants(U0) is non empty
  Subset of U2 by Th15;
  then
A1: Constants(U0) c= (the carrier of U1) /\ (the carrier of U2) by XBOOLE_1:19;
  thus thesis by A1;
end;

definition
  let U0 be Universal_Algebra, A be Subset of U0;
  assume
A1: Constants(U0) <> {} or A <> {};
  func GenUnivAlg(A) -> strict SubAlgebra of U0 means
  :Def12:
  A c= the carrier
  of it & for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds it is
  SubAlgebra of U1;
  existence
  proof
    defpred P[set] means A c= $1 & Constants(U0) c= $1 &
        for B be non empty Subset of U0 st B =$1 holds B is opers_closed;
    set C = bool(the carrier of U0);
    consider X be set such that
A2: for x holds x in X iff x in C & P[x] from XFAMILY:sch 1;
    set P = meet X;
    the carrier of U0 in C & for B be non empty Subset of U0 st B = the
    carrier of U0 holds B is opers_closed by Th4,ZFMISC_1:def 1;
    then
A3: the carrier of U0 in X by A2;
A4: P c= the carrier of U0
    by A3,SETFAM_1:def 1;
    now
      let x be set;
      assume x in X;
      then A c= x & Constants(U0) c= x by A2;
      hence A \/ Constants(U0) c= x by XBOOLE_1:8;
    end;
    then
A5: A \/ Constants(U0) c= P by A3,SETFAM_1:5;
    then reconsider P as non empty Subset of U0 by A1,A4;
    take E = UniAlgSetClosed(P);
A6: P is opers_closed
    proof
      let o be operation of U0;
      let s be FinSequence of P;
      assume
A7:   len s = arity o;
      now
        let a be set;
A8:     rng s c= P by FINSEQ_1:def 4;
        assume
A9:     a in X;
        then reconsider a0 = a as Subset of U0 by A2;
        A c= a0 & Constants(U0) c= a0 by A2,A9;
        then reconsider a0 as non empty Subset of U0 by A1;
        P c= a0 by A9,SETFAM_1:3;
        then rng s c= a0 by A8;
        then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;
        a0 is opers_closed by A2,A9;
        then a0 is_closed_on o;
        then o.s0 in a0 by A7;
        hence o.s in a;
      end;
      hence thesis by A3,SETFAM_1:def 1;
    end;
    then
A10: E = UAStr (# P, Opers(U0,P) #) by Def8;
    A c= A \/ Constants(U0) by XBOOLE_1:7;
    hence A c= the carrier of E by A5,A10;
    let U1 be SubAlgebra of U0;
    assume
A11: A c= the carrier of U1;
    set u1 = the carrier of U1;
A12: Constants(U0) c= u1
    proof
      reconsider B =u1 as non empty Subset of U0 by Def7;
      let x be object;
      assume x in Constants(U0);
      then consider a be Element of U0 such that
A13:  a=x and
A14:  ex o be operation of U0 st arity o=0 & a in rng o;
      consider o0 be operation of U0 such that
A15:  arity o0 = 0 and
A16:  a in rng o0 by A14;
      consider y be object such that
A17:  y in dom o0 and
A18:  a = o0.y by A16,FUNCT_1:def 3;
      dom o0 = 0-tuples_on the carrier of U0 by A15,MARGREL1:22
        .= {<*>the carrier of U0} by FINSEQ_2:94;
      then y in {<*>B} by A17;
      then y in 0-tuples_on B by FINSEQ_2:94;
      then y in dom o0 /\ (arity o0)-tuples_on B by A15,A17,XBOOLE_0:def 4;
      then
A19:  y in dom (o0 | (arity o0)-tuples_on B) by RELAT_1:61;
      consider n being Nat such that
A20:  n in dom (the charact of(U0)) and
A21:  (the charact of U0).n=o0 by FINSEQ_2:10;
A22:  n in dom the charact of(U1) by A20,Th7;
      then reconsider o1= (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
      the charact of(U1) =Opers(U0,B) by Def7;
      then
A23:  o1=o0/.B by A21,A22,Def6;
      B is opers_closed by Def7;
      then
A24:  B is_closed_on o0;
      then y in dom (o0/.B) by A19,Def5;
      then
A25:  o1.y in rng o1 by A23,FUNCT_1:def 3;
A26:  rng o1 c= the carrier of U1 by RELAT_1:def 19;
      o1.y = (o0 | (arity o0)-tuples_on B).y by A23,A24,Def5
        .= a by A18,A19,FUNCT_1:47;
      hence thesis by A13,A25,A26;
    end;
    u1 is Subset of U0 & for B be non empty Subset of U0 st B = u1 holds
    B is opers_closed by Def7;
    then
A27: u1 in X by A2,A11,A12;
    hence the carrier of E is Subset of U1 by A10,SETFAM_1:3;
    let B be non empty Subset of U1;
    assume
A28: B = the carrier of E;
    reconsider u11 = u1 as non empty Subset of U0 by Def7;
A29: the charact of(U1) = Opers(U0,u11) by Def7;
A30: dom the charact of(U0) = dom Opers(U0,u11) by Def6;
A31: u11 is opers_closed by Def7;
A32: now
      let o1 be operation of U1;
      consider n being Nat such that
A33:  n in dom the charact of(U1) and
A34:  o1 = (the charact of U1).n by FINSEQ_2:10;
      reconsider o0 = (the charact of U0).n as operation of U0 by A29,A30,A33,
FUNCT_1:def 3;
A35:  arity o0 =arity o1 by A33,A34,Th6;
A36:  u11 is_closed_on o0 by A31;
      now
        let s be FinSequence of B;
A37:    P is_closed_on o0 by A6;
        reconsider sE=s as Element of P* by A10,A28,FINSEQ_1:def 11;
        s is FinSequence of u11 by FINSEQ_2:24;
        then reconsider s1 =s as Element of u11* by FINSEQ_1:def 11;
A38:    dom(o0|(arity o0)-tuples_on u11) = (dom o0) /\ (arity o0)
        -tuples_on u11 by RELAT_1:61
          .= (arity o0)-tuples_on (the carrier of U0) /\ (arity o0)
        -tuples_on u11 by MARGREL1:22
          .= (arity o0)-tuples_on u11 by MARGREL1:21;
        assume
A39:    len s = arity o1;
        then s1 in{q where q is Element of u11*: len q = arity o0} by A35;
        then
A40:    s1 in dom(o0|(arity o0)-tuples_on u11) by A38,FINSEQ_2:def 4;
        o1.s = (o0/.u11).s1 by A29,A33,A34,Def6
          .= (o0|(arity o0)-tuples_on u11).s1 by A36,Def5
          .= o0.sE by A40,FUNCT_1:47;
        hence o1.s in B by A10,A28,A35,A39,A37;
      end;
      hence B is_closed_on o1;
    end;
A41: dom Opers(U1,B) = dom the charact of(U1) by Def6;
A42: dom the charact of(U0) = dom Opers(U0,P) by Def6;
A43: P c= u1 by A27,SETFAM_1:3;
    now
      let n be Nat;
      assume
A44:  n in dom the charact of(U0);
      then reconsider o0 = (the charact of U0).n as operation of U0 by
FUNCT_1:def 3;
      reconsider o1 = (the charact of U1).n as operation of U1 by A29,A30,A44,
FUNCT_1:def 3;
A45:  u11 is_closed_on o0 by A31;
A46:  P is_closed_on o0 by A6;
      thus (the charact of E).n = o0/.P by A10,A42,A44,Def6
        .= o0|((arity o0)-tuples_on P) by A46,Def5
        .= o0|((arity o0)-tuples_on u11 /\(arity o0)-tuples_on P)
              by A43,MARGREL1:21
        .= (o0|((arity o0)-tuples_on u11))|((arity o0)-tuples_on P) by
RELAT_1:71
        .= (o0/.u11)|((arity o0)-tuples_on P) by A45,Def5
        .= o1|((arity o0)-tuples_on P) by A29,A30,A44,Def6
        .= o1|((arity o1)-tuples_on B) by A10,A28,A29,A30,A44,Th6
        .= o1/.B by A32,Def5
        .= Opers(U1,B).n by A29,A30,A41,A44,Def6;
    end;
    hence thesis by A10,A29,A42,A30,A32,A41,FINSEQ_1:13;
  end;
  uniqueness
  proof
    let W1,W2 be strict SubAlgebra of U0;
    assume A c= the carrier of W1 & ( for U1 be SubAlgebra of U0 st A c= the
carrier of U1 holds W1 is SubAlgebra of U1)& A c= the carrier of W2 & for U2 be
    SubAlgebra of U0 st A c= the carrier of U2 holds W2 is SubAlgebra of U2;
    then W1 is strict SubAlgebra of W2 & W2 is strict SubAlgebra of W1;
    hence thesis by Th10;
  end;
end;

theorem
  for U0 be strict Universal_Algebra holds GenUnivAlg([#](the carrier of
  U0)) = U0
proof
  let U0 be strict Universal_Algebra;
  set W = GenUnivAlg([#](the carrier of U0));
  reconsider B = the carrier of W as non empty Subset of U0 by Def7;
  (the carrier of W) is Subset of U0 & the carrier of U0 c= the carrier of
  W by Def7,Def12;
  then
A1: the carrier of U0 = the carrier of W;
A2: dom the charact of(U0) = dom Opers(U0,B) by Def6;
A3: for n being Nat st n in dom the charact of(U0) holds (the charact of(U0)
  ).n = (Opers(U0,B)).n
  proof
    let n be Nat;
    assume
A4: n in dom the charact of(U0);
    then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
    (Opers(U0,B)).n = o/.B by A2,A4,Def6;
    hence thesis by A1,Th4;
  end;
  the charact of(W) = Opers(U0,B) by Def7;
  hence thesis by A1,A2,A3,FINSEQ_1:13;
end;

theorem Th19:
  for U0 be Universal_Algebra, U1 be strict SubAlgebra of U0, B be
  non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg(B) = U1
proof
  let U0 be Universal_Algebra,U1 be strict SubAlgebra of U0, B be non empty
  Subset of U0;
  set W = GenUnivAlg(B);
  assume
A1: B = the carrier of U1;
  then GenUnivAlg(B) is SubAlgebra of U1 by Def12;
  then
A2: the carrier of W is non empty Subset of U1 by Def7;
  the carrier of U1 c= the carrier of W by A1,Def12;
  then the carrier of U1 = the carrier of W by A2;
  hence thesis by Th12;
end;

definition
  let U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0;
  func U1 "\/" U2 -> strict SubAlgebra of U0 means
  :Def13:
  for A be non empty
  Subset of U0 st A = (the carrier of U1) \/ (the carrier of U2) holds it =
  GenUnivAlg(A);
  existence
  proof
    reconsider B =(the carrier of U1) \/ (the carrier of U2) as non empty set;
    the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
    by Def7;
    then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
    take GenUnivAlg(B);
    thus thesis;
  end;
  uniqueness
  proof
    reconsider B =(the carrier of U1) \/ (the carrier of U2) as non empty set;
    let W1,W2 be strict SubAlgebra of U0;
    assume that
A1: for A be non empty Subset of U0 st A = (the carrier of U1) \/ (the
    carrier of U2) holds W1 = GenUnivAlg(A) and
A2: for A be non empty Subset of U0 st A = (the carrier of U1) \/ (the
    carrier of U2) holds W2 = GenUnivAlg(A);
    the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
    by Def7;
    then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
    W1 = GenUnivAlg(B) by A1;
    hence thesis by A2;
  end;
end;

theorem Th20:
  for U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be
  Subset of U0 st (A <> {} or Constants(U0) <> {}) & B = A \/ the carrier of U1
  holds GenUnivAlg(A) "\/" U1 = GenUnivAlg(B)
proof
  let U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be Subset of U0;
  reconsider u1 = the carrier of U1, a = the carrier of GenUnivAlg(A) as non
  empty Subset of U0 by Def7;
  assume that
A1: A <> {} or Constants(U0) <> {} and
A2: B = A \/ the carrier of U1;
A3: A c= the carrier of GenUnivAlg(A) by Def12;
A4: B c= the carrier of GenUnivAlg(B) by Def12;
  A c=B by A2,XBOOLE_1:7;
  then
A5: A c= the carrier of GenUnivAlg( B) by A4;
  now
    per cases by A1;
    case
      A <> {};
      hence
      (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) <>
      {} by A3,A5,XBOOLE_1:3,19;
    end;
    case
A6:   Constants(U0) <> {};
      Constants(U0) is Subset of GenUnivAlg(A) & Constants(U0) is Subset
      of GenUnivAlg(B) by Th15;
      hence
      (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) <>
      {} by A6,XBOOLE_1:3,19;
    end;
  end;
  then (the carrier of GenUnivAlg(A)) meets (the carrier of GenUnivAlg(B));
  then
A7: the carrier of (GenUnivAlg(A) /\ GenUnivAlg(B)) = (the carrier of
  GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) by Def9;
  reconsider b=a \/ u1 as non empty Subset of U0;
A8: (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) c= a
  by XBOOLE_1:17;
  A c= (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B) )
  by A3,A5,XBOOLE_1:19;
  then GenUnivAlg(A) is SubAlgebra of (GenUnivAlg(A) /\ GenUnivAlg(B)) by A1,A7
,Def12;
  then a is non empty Subset of (GenUnivAlg(A) /\ GenUnivAlg(B)) by Def7;
  then a= (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) by
A7,A8;
  then
A9: a c= the carrier of GenUnivAlg(B) by XBOOLE_1:17;
  u1 c= B by A2,XBOOLE_1:7;
  then u1 c= the carrier of GenUnivAlg(B) by A4;
  then b c= the carrier of GenUnivAlg(B) by A9,XBOOLE_1:8;
  then
A10: GenUnivAlg(b) is strict SubAlgebra of GenUnivAlg(B) by Def12;
A11: (GenUnivAlg(A) "\/" U1) = GenUnivAlg(b) by Def13;
  then
A12: a \/ u1 c= the carrier of (GenUnivAlg(A)"\/"U1) by Def12;
  A \/ u1 c= a \/ u1 by A3,XBOOLE_1:13;
  then B c=the carrier of (GenUnivAlg(A)"\/"U1) by A2,A12;
  then GenUnivAlg(B) is strict SubAlgebra of (GenUnivAlg(A)"\/"U1) by A2,Def12;
  hence thesis by A11,A10,Th10;
end;

theorem Th21:
  for U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0 holds U1
  "\/" U2 = U2 "\/" U1
proof
  let U0 be Universal_Algebra ,U1,U2 be SubAlgebra of U0;
  reconsider u1=the carrier of U1,u2=the carrier of U2 as non empty Subset of
  U0 by Def7;
  reconsider A = u1 \/ u2 as non empty Subset of U0;
  U1 "\/" U2 = GenUnivAlg(A) by Def13;
  hence thesis by Def13;
end;

theorem Th22:
  for U0 be with_const_op Universal_Algebra,U1,U2 be strict
  SubAlgebra of U0 holds U1 /\ (U1"\/"U2) = U1
proof
  let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;
  reconsider u112=the carrier of(U1 /\ (U1"\/"U2)) as non empty Subset of U0
  by Def7;
  reconsider u1= the carrier of U1,u2 =the carrier of U2 as non empty Subset
  of U0 by Def7;
  reconsider A= u1 \/ u2 as non empty Subset of U0;
A1: the charact of (U1)= Opers(U0,u1) by Def7;
A2: dom Opers(U0,u1) = dom the charact of(U0) by Def6;
  U1"\/"U2 = GenUnivAlg(A) by Def13;
  then
A3: A c= the carrier of (U1 "\/" U2) by Def12;
A4: (the carrier of U1) meets (the carrier of (U1"\/"U2)) by Th17;
  then
A5: the carrier of (U1 /\(U1"\/"U2))=(the carrier of U1)/\ (the carrier of(
  U1 "\/" U2)) by Def9;
  then
A6: the carrier of (U1 /\(U1"\/"U2)) c= the carrier of U1 by XBOOLE_1:17;
  the carrier of U1 c= A by XBOOLE_1:7;
  then the carrier of U1 c= the carrier of (U1"\/"U2) by A3;
  then
A7: the carrier of U1 c=the carrier of (U1 /\(U1"\/"U2)) by A5,XBOOLE_1:19;
A8: dom Opers(U0,u112) = dom the charact of(U0) by Def6;
A9: for n being Nat st n in dom the charact of (U0) holds (the charact of
  U1/\(U1"\/"U2)).n= (the charact of U1).n
  proof
    let n be Nat;
    assume
A10: n in dom the charact of (U0);
    then reconsider o0 = (the charact of U0).n as operation of U0 by
FUNCT_1:def 3;
    thus (the charact of U1 /\ ( U1 "\/" U2)).n = Opers(U0,u112).n by A4,Def9
      .= o0/.u112 by A8,A10,Def6
      .=o0/.u1 by A7,A6,XBOOLE_0:def 10
      .=Opers(U0,u1).n by A2,A10,Def6
      .= (the charact of U1).n by Def7;
  end;
  the charact of (U1/\(U1"\/"U2)) = Opers(U0,u112) by A4,Def9;
  then the charact of (U1/\(U1"\/"U2))= the charact of (U1) by A1,A8,A2,A9,
FINSEQ_1:13;
  hence thesis by A7,A6,XBOOLE_0:def 10;
end;

theorem Th23:
  for U0 be with_const_op Universal_Algebra,U1,U2 be strict
  SubAlgebra of U0 holds (U1 /\ U2)"\/"U2 = U2
proof
  let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;
  reconsider u12= the carrier of (U1 /\ U2), u2 = the carrier of U2 as non
  empty Subset of U0 by Def7;
  reconsider A=u12 \/ u2 as non empty Subset of U0;
  (the carrier of U1) meets (the carrier of U2) by Th17;
  then u12 = (the carrier of U1) /\ (the carrier of U2) by Def9;
  then
A1: u12 c= u2 by XBOOLE_1:17;
  (U1 /\ U2)"\/"U2=GenUnivAlg(A) by Def13;
  hence thesis by A1,Th19,XBOOLE_1:12;
end;

definition
  let U0 be Universal_Algebra;
  func Sub(U0) -> set means
  :Def14:
  for x being object holds x in it iff x is strict SubAlgebra of U0;
  existence
  proof
    reconsider X = { GenUnivAlg(A) where A is Subset of U0: A is non empty} as
    set;
    take X;
    let x be object;
    thus x in X implies x is strict SubAlgebra of U0
    proof
      assume x in X;
      then ex A be Subset of U0 st x = GenUnivAlg(A) & A is non empty;
      hence thesis;
    end;
    assume x is strict SubAlgebra of U0;
    then reconsider a = x as strict SubAlgebra of U0;
    reconsider A = the carrier of a as non empty Subset of U0 by Def7;
    a = GenUnivAlg(A) by Th19;
    hence thesis;
  end;
  uniqueness
  proof
    let A,B be set;
    assume that
A1: for x being object holds x in A iff x is strict SubAlgebra of U0 and
A2: for y being object holds y in B iff y is strict SubAlgebra of U0;
    now
      let x be object;
      assume x in A;
      then x is strict SubAlgebra of U0 by A1;
      hence x in B by A2;
    end;
    hence A c= B;
    let y be object;
    assume y in B;
    then y is strict SubAlgebra of U0 by A2;
    hence thesis by A1;
  end;
end;

registration
  let U0 be Universal_Algebra;
  cluster Sub(U0) -> non empty;
  coherence
  proof
    set x = the strict SubAlgebra of U0;
    x in Sub U0 by Def14;
    hence thesis;
  end;
end;

definition
  let U0 be Universal_Algebra;
  func UniAlg_join(U0) -> BinOp of Sub(U0) means
  :Def15:
  for x,y be Element of
Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it.
  (x,y) = U1 "\/" U2;
  existence
  proof
    defpred P[(Element of Sub(U0)),(Element of Sub(U0)),Element of Sub(U0)]
means for U1,U2 be strict SubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 "\/" U2
    ;
A1: for x,y being Element of Sub(U0) ex z being Element of Sub(U0) st P[x, y,z]
    proof
      let x,y be Element of Sub(U0);
      reconsider U1=x, U2=y as strict SubAlgebra of U0 by Def14;
      reconsider z =U1"\/"U2 as Element of Sub(U0) by Def14;
      take z;
      thus thesis;
    end;
    consider o be BinOp of Sub(U0) such that
A2: for a,b be Element of Sub(U0) holds P[a,b,o.(a,b)] from BINOP_1:
    sch 3 (A1);
    take o;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of (Sub(U0));
    assume that
A3: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
    of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 "\/" U2 and
A4: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
    of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 "\/" U2;
    for x be Element of Sub(U0) for y be Element of Sub(U0) holds o1.(x,y)
    = o2.(x,y)
    proof
      let x,y be Element of Sub(U0);
      reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
      o1.(x,y) = U1"\/" U2 by A3;
      hence thesis by A4;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let U0 be Universal_Algebra;
  func UniAlg_meet(U0) -> BinOp of Sub(U0) means
  :Def16:
  for x,y be Element of
Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it.
  (x,y) = U1 /\ U2;
  existence
  proof
    defpred P[(Element of Sub(U0)),(Element of Sub(U0)),Element of Sub(U0)]
means for U1,U2 be strict SubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 /\ U2;
A1: for x,y being Element of Sub(U0) ex z being Element of Sub(U0) st P[x, y,z]
    proof
      let x,y be Element of Sub(U0);
      reconsider U1=x, U2=y as strict SubAlgebra of U0 by Def14;
      reconsider z =U1 /\ U2 as Element of Sub(U0) by Def14;
      take z;
      thus thesis;
    end;
    consider o be BinOp of Sub(U0) such that
A2: for a,b be Element of Sub(U0) holds P[a,b,o.(a,b)] from BINOP_1:
    sch 3 (A1);
    take o;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of (Sub(U0));
    assume that
A3: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
    of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 /\ U2 and
A4: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
    of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 /\ U2;
    for x be Element of Sub(U0) for y be Element of Sub(U0) holds o1.(x,y)
    = o2.(x,y)
    proof
      let x,y be Element of Sub(U0);
      reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
      o1.(x,y) = U1 /\ U2 by A3;
      hence thesis by A4;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

theorem Th24:
  UniAlg_join(U0) is commutative
proof
  set o = UniAlg_join(U0);
  for x,y be Element of Sub(U0) holds o.(x,y)=o.(y,x)
  proof
    let x,y be Element of Sub(U0);
    reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
    reconsider B=(the carrier of U1) \/ (the carrier of U2) as non empty set;
    the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
    by Def7;
    then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
A1: U1"\/" U2 = GenUnivAlg(B) by Def13;
    o.(x,y) = U1 "\/" U2 & o.(y,x) = U2 "\/" U1 by Def15;
    hence thesis by A1,Def13;
  end;
  hence thesis by BINOP_1:def 2;
end;

theorem Th25:
  UniAlg_join(U0) is associative
proof
  set o = UniAlg_join(U0);
  for x,y,z be Element of Sub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
  proof
    let x,y,z be Element of Sub(U0);
    reconsider U1=x,U2=y,U3=z as strict SubAlgebra of U0 by Def14;
    reconsider B=(the carrier of U1) \/ ((the carrier of U2) \/ (the carrier
    of U3)) as non empty set;
A1: o.(x,y)=U1"\/"U2 by Def15;
A2: the carrier of U2 is Subset of U0 by Def7;
A3: the carrier of U3 is Subset of U0 by Def7;
    then reconsider
    C = (the carrier of U2) \/ (the carrier of U3) as non empty
    Subset of U0 by A2,XBOOLE_1:8;
A4: the carrier of U1 is Subset of U0 by Def7;
    then reconsider D=(the carrier of U1) \/ (the carrier of U2) as non empty
    Subset of U0 by A2,XBOOLE_1:8;
    (the carrier of U2) \/ (the carrier of U3) c= the carrier of U0 by A2,A3,
XBOOLE_1:8;
    then reconsider B as non empty Subset of U0 by A4,XBOOLE_1:8;
A5: B= D \/ (the carrier of U3) by XBOOLE_1:4;
A6: (U1"\/"U2)"\/"U3 = GenUnivAlg(D)"\/" U3 by Def13
      .= GenUnivAlg(B) by A5,Th20;
    o.(y,z)=U2"\/"U3 by Def15;
    then
A7: o.(x,o.(y,z)) = U1 "\/" (U2"\/"U3) by Def15;
    U1"\/" (U2"\/"U3) = U1 "\/"(GenUnivAlg(C)) by Def13
      .=(GenUnivAlg(C)) "\/" U1 by Th21
      .= GenUnivAlg(B) by Th20;
    hence thesis by A1,A7,A6,Def15;
  end;
  hence thesis by BINOP_1:def 3;
end;

theorem Th26:
  for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0)
  is commutative
proof
  let U0 be with_const_op Universal_Algebra;
  set o = UniAlg_meet(U0);
  for x,y be Element of Sub(U0) holds o.(x,y)=o.(y,x)
  proof
    let x,y be Element of Sub(U0);
    reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
A1: o.(x,y) = U1 /\ U2 & o.(y,x) = U2 /\ U1 by Def16;
A2: (the carrier of U1) meets (the carrier of U2) by Th17;
    then
    the carrier of(U2 /\ U1) = (the carrier of U2) /\ (the carrier of U1)
    & for B2 be non empty Subset of U0 st B2=the carrier of (U2/\U1) holds the
    charact of (U2/\U1) = Opers(U0,B2) & B2 is opers_closed by Def9;
    hence thesis by A1,A2,Def9;
  end;
  hence thesis by BINOP_1:def 2;
end;

theorem Th27:
  for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0)
  is associative
proof
  let U0 be with_const_op Universal_Algebra;
  set o = UniAlg_meet(U0);
  for x,y,z be Element of Sub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
  proof
    let x,y,z be Element of Sub(U0);
    reconsider U1=x,U2=y,U3=z as strict SubAlgebra of U0 by Def14;
    reconsider u23 = U2 /\ U3,u12 =U1 /\ U2 as Element of Sub(U0) by Def14;
A1: o.(x,o.(y,z)) =o.(x,u23) by Def16
      .= U1/\(U2 /\ U3) by Def16;
A2: o.(o.(x,y),z) = o.(u12,z) by Def16
      .=(U1 /\ U2) /\ U3 by Def16;
    (the carrier of U2) meets (the carrier of U3) by Th17;
    then
A3: the carrier of(U2 /\ U3) = (the carrier of U2) /\ (the carrier of U3)
    by Def9;
    then
A4: (the carrier of U1) meets ((the carrier of U2)/\(the carrier of U3))
    by Th17;
    then
A5: for B be non empty Subset of U0 st B=the carrier of (U1/\(U2/\U3))
holds the charact of (U1/\(U2/\U3)) = Opers(U0,B) & B is opers_closed by A3
,Def9;
A6: the carrier of (U1 /\ (U2 /\ U3)) =(the carrier of U1) /\ ((the
    carrier of U2)/\(the carrier of U3)) by A3,A4,Def9;
    then reconsider
    C =(the carrier of U1) /\ ((the carrier of U2)/\ (the carrier
    of U3)) as non empty Subset of U0 by Def7;
A7: C =((the carrier of U1)/\(the carrier of U2)) /\ (the carrier of U3)
    by XBOOLE_1:16;
    (the carrier of U1) meets (the carrier of U2) by Th17;
    then
A8: the carrier of (U1 /\ U2) = (the carrier of U1) /\ (the carrier of U2)
    by Def9;
    then
    ((the carrier of U1) /\ (the carrier of U2)) meets (the carrier of U3)
    by Th17;
    hence thesis by A1,A2,A8,A6,A5,A7,Def9;
  end;
  hence thesis by BINOP_1:def 3;
end;

definition
  let U0 be with_const_op Universal_Algebra;
  func UnSubAlLattice(U0) -> strict Lattice equals
  LattStr (# Sub(U0),
    UniAlg_join(U0), UniAlg_meet(U0) #);
  coherence
  proof
    set L = LattStr (# Sub(U0), UniAlg_join(U0), UniAlg_meet(U0) #);
A1: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
    proof
      let a,b,c be Element of L;
      reconsider x=a,y=b,z=c as Element of Sub(U0);
A2:   UniAlg_join(U0) is associative by Th25;
      thus a"\/"(b"\/"c) = (the L_join of L).(a,(b"\/"c)) by LATTICES:def 1
        .= (UniAlg_join(U0)).(x,(UniAlg_join(U0)).(y,z)) by LATTICES:def 1
        .=(the L_join of L).((the L_join of L).(a,b),c) by A2,BINOP_1:def 3
        .=((the L_join of L).(a,b))"\/"c by LATTICES:def 1
        .=(a"\/"b)"\/"c by LATTICES:def 1;
    end;
A3: for a,b being Element of L holds a"/\"b = b"/\"a
    proof
      let a,b be Element of L;
      reconsider x=a,y=b as Element of Sub(U0);
A4:   UniAlg_meet(U0) is commutative by Th26;
      thus a"/\"b = (UniAlg_meet(U0)).(x,y) by LATTICES:def 2
        .=(the L_meet of L).(b,a) by A4,BINOP_1:def 2
        .=b"/\"a by LATTICES:def 2;
    end;
A5: for a,b being Element of L holds a"/\"(a"\/"b)=a
    proof
      let a,b be Element of L;
      reconsider x=a,y=b as Element of Sub(U0);
A6:   (UniAlg_meet(U0)).(x,(UniAlg_join(U0)).(x,y))= x
      proof
        reconsider U1= x,U2=y as strict SubAlgebra of U0 by Def14;
        (UniAlg_join(U0)).(x,y) = U1"\/"U2 by Def15;
        hence
        (UniAlg_meet(U0)).(x,(UniAlg_join(U0)).(x,y)) = (U1 /\( U1"\/"U2)
        ) by Def16
          .=x by Th22;
      end;
      thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
        .=a by A6,LATTICES:def 1;
    end;
A7: for a,b being Element of L holds (a"/\"b)"\/"b = b
    proof
      let a,b be Element of L;
      reconsider x=a,y=b as Element of Sub(U0);
A8:   (UniAlg_join(U0)).((UniAlg_meet(U0)).(x,y),y)= y
      proof
        reconsider U1= x,U2=y as strict SubAlgebra of U0 by Def14;
        (UniAlg_meet(U0)).(x,y) = U1 /\ U2 by Def16;
        hence
        (UniAlg_join(U0)).((UniAlg_meet(U0)).(x,y),y) = ((U1 /\ U2)"\/"U2
        ) by Def15
          .=y by Th23;
      end;
      thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
        .=b by A8,LATTICES:def 2;
    end;
A9: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
    proof
      let a,b,c be Element of L;
      reconsider x=a,y=b,z=c as Element of Sub(U0);
A10:  UniAlg_meet(U0) is associative by Th27;
      thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
        .= (UniAlg_meet(U0)).(x,(UniAlg_meet(U0)).(y,z)) by LATTICES:def 2
        .=(the L_meet of L).((the L_meet of L).(a,b),c) by A10,BINOP_1:def 3
        .=((the L_meet of L).(a,b))"/\"c by LATTICES:def 2
        .=(a"/\"b)"/\"c by LATTICES:def 2;
    end;
    for a,b being Element of L holds a"\/"b = b"\/"a
    proof
      let a,b be Element of L;
      reconsider x=a,y=b as Element of Sub(U0);
A11:  UniAlg_join(U0) is commutative by Th24;
      thus a"\/"b = (UniAlg_join(U0)).(x,y) by LATTICES:def 1
        .=(the L_join of L).(b,a) by A11,BINOP_1:def 2
        .=b"\/"a by LATTICES:def 1;
    end;
    then L is join-commutative join-associative meet-absorbing
    meet-commutative meet-associative join-absorbing by A1,A7,A3,A9,A5,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
    hence thesis;
  end;
end;