:: UNIALG_3 semantic presentation

begin


definition
let U0 be Universal_Algebra;
mode SubAlgebra-Family of U0 ->  set  means :Def1: :: UNIALG_3:def 1
 for U1 being set st U1 in it holds
U1 is SubAlgebra of U0;
existence
 ex b1 being set st
for U1 being set st U1 in b1 holds
U1 is SubAlgebra of U0
proof
take  {} ; ::_thesis: for U1 being set st U1 in {} holds
U1 is SubAlgebra of U0
thus  for U1 being set st U1 in {} holds
U1 is SubAlgebra of U0 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines SubAlgebra-Family UNIALG_3:def_1_:_
 for U0 being Universal_Algebra
for b2 being set holds
( b2 is SubAlgebra-Family of U0 iff for U1 being set st U1 in b2 holds
U1 is SubAlgebra of U0 );

registration
let U0 be Universal_Algebra;
cluster non empty for SubAlgebra-Family of U0;
existence
 not for b1 being SubAlgebra-Family of U0 holds b1 is empty
proof
set U1 = the SubAlgebra of U0;
 for U2 being set st U2 in { the SubAlgebra of U0} holds
U2 is SubAlgebra of U0 by TARSKI:def_1;
then reconsider U00 = { the SubAlgebra of U0} as SubAlgebra-Family of U0 by Def1;
take  U00 ; ::_thesis: not U00 is empty
thus  not U00 is empty ; ::_thesis: verum
end;
end;

definition
let U0 be Universal_Algebra;
:: original: Sub
redefine func Sub U0 ->  non empty SubAlgebra-Family of U0;
coherence
 Sub U0 is non empty SubAlgebra-Family of U0
proof
 Sub U0 is SubAlgebra-Family of U0
proof
let U1 be set ; :: according to UNIALG_3:def_1 ::_thesis: ( U1 in Sub U0 implies U1 is SubAlgebra of U0 )
assume  U1 in Sub U0 ; ::_thesis: U1 is SubAlgebra of U0
hence  U1 is SubAlgebra of U0 by UNIALG_2:def_14; ::_thesis: verum
end;
hence  Sub U0 is non empty SubAlgebra-Family of U0 ; ::_thesis: verum
end;
let U00 be non empty SubAlgebra-Family of U0;
:: original: Element
redefine mode Element of U00 ->  SubAlgebra of U0;
coherence
 for b1 being Element of U00 holds b1 is SubAlgebra of U0 by Def1;
end;

definition
let U0 be Universal_Algebra;
let u be Element of Sub U0;
func carr u ->  Subset of U0 means :Def2: :: UNIALG_3:def 2
 ex U1 being SubAlgebra of U0 st
( u = U1 & it = the carrier of U1 );
existence
 ex b1 being Subset of U0 ex U1 being SubAlgebra of U0 st
( u = U1 & b1 = the carrier of U1 )
proof
consider U1 being 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 ; ::_thesis: ex U1 being SubAlgebra of U0 st
( u = U1 & A = the carrier of U1 )
take  U1 ; ::_thesis: ( u = U1 & A = the carrier of U1 )
thus  ( u = U1 & A = the carrier of U1 ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of U0 st ex U1 being SubAlgebra of U0 st
( u = U1 & b1 = the carrier of U1 ) & ex U1 being SubAlgebra of U0 st
( u = U1 & b2 = the carrier of U1 ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines carr UNIALG_3:def_2_:_
 for U0 being Universal_Algebra
for u being Element of Sub U0
for b3 being Subset of U0 holds
( b3 = carr u iff ex U1 being SubAlgebra of U0 st
( u = U1 & b3 = the carrier of U1 ) );

definition
let U0 be Universal_Algebra;
func Carr U0 ->  Function of (Sub U0),(bool the carrier of U0) means :Def3: :: UNIALG_3:def 3
 for u being Element of Sub U0 holds it . u = carr u;
existence
 ex b1 being Function of (Sub U0),(bool the carrier of U0) st
for u being Element of Sub U0 holds b1 . u = carr u
proof
deffunc H1( Element of Sub U0) ->  Subset of U0 = carr $1;
 ex f being Function of (Sub U0),(bool the carrier of U0) st
for x being Element of Sub U0 holds f . x = H1(x) from FUNCT_2:sch_4();
hence  ex b1 being Function of (Sub U0),(bool the carrier of U0) st
for u being Element of Sub U0 holds b1 . u = carr u ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Sub U0),(bool the carrier of U0) st ( for u being Element of Sub U0 holds b1 . u = carr u ) & ( for u being Element of Sub U0 holds b2 . u = carr u ) holds
b1 = b2
proof
let F1, F2 be Function of (Sub U0),(bool the carrier of U0); ::_thesis: ( ( for u being Element of Sub U0 holds F1 . u = carr u ) & ( for u being Element of Sub U0 holds F2 . u = carr u ) implies F1 = F2 )
assume that
A1: for u1 being Element of Sub U0 holds F1 . u1 = carr u1 and
A2: for u2 being Element of Sub U0 holds F2 . u2 = carr u2 ; ::_thesis: F1 = F2
 for u being set st u in Sub U0 holds
F1 . u = F2 . u
proof
let u be set ; ::_thesis: ( u in Sub U0 implies F1 . u = F2 . u )
assume  u in Sub U0 ; ::_thesis: F1 . u = F2 . u
then reconsider u1 = u as Element of Sub U0 ;
consider U1 being 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  F1 . u = F2 . u by A2, A3; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Carr UNIALG_3:def_3_:_
 for U0 being Universal_Algebra
for b2 being Function of (Sub U0),(bool the carrier of U0) holds
( b2 = Carr U0 iff for u being Element of Sub U0 holds b2 . u = carr u );

theorem Th1: :: UNIALG_3:1
for U0 being Universal_Algebra
for u being set holds
( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )
proof
let U0 be Universal_Algebra; ::_thesis: for u being set holds
( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )
let u be set ; ::_thesis: ( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )
thus  ( u in Sub U0 implies ex U1 being strict SubAlgebra of U0 st u = U1 ) ::_thesis: ( ex U1 being strict SubAlgebra of U0 st u = U1 implies u in Sub U0 )
proof
assume  u in Sub U0 ; ::_thesis: ex U1 being strict SubAlgebra of U0 st u = U1
then  u is strict SubAlgebra of U0 by UNIALG_2:def_14;
hence  ex U1 being strict SubAlgebra of U0 st u = U1 ; ::_thesis: verum
end;
thus  ( ex U1 being strict SubAlgebra of U0 st u = U1 implies u in Sub U0 ) by UNIALG_2:def_14; ::_thesis: verum
end;

theorem :: UNIALG_3:2
for U0 being Universal_Algebra
for H being non empty Subset of U0
for o being operation of U0 st arity o = 0 holds
( H is_closed_on o iff o . {} in H )
proof
let U0 be Universal_Algebra; ::_thesis: for H being non empty Subset of U0
for o being operation of U0 st arity o = 0 holds
( H is_closed_on o iff o . {} in H )
let H be non empty Subset of U0; ::_thesis: for o being operation of U0 st arity o = 0 holds
( H is_closed_on o iff o . {} in H )
let o be operation of U0; ::_thesis: ( arity o = 0 implies ( H is_closed_on o iff o . {} in H ) )
assume A1: arity o = 0 ; ::_thesis: ( H is_closed_on o iff o . {} in H )
thus  ( H is_closed_on o implies o . {} in H ) ::_thesis: ( o . {} in H implies H is_closed_on o )
proof
assume A2: H is_closed_on o ; ::_thesis: o . {} in H
consider s being FinSequence of H such that
A3: len s = arity o by FINSEQ_1:19;
 s = {} by A1, A3;
hence  o . {} in H by A2, A3, UNIALG_2:def_3; ::_thesis: verum
end;
thus  ( o . {} in H implies H is_closed_on o ) ::_thesis: verum
proof
assume A4: o . {} in H ; ::_thesis: H is_closed_on o
let s be FinSequence of H; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in H )
assume  len s = arity o ; ::_thesis: o . s in H
then  s = {} by A1;
hence  o . s in H by A4; ::_thesis: verum
end;
end;

theorem Th3: :: UNIALG_3:3
for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0
proof
let U0 be Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0
let U1 be SubAlgebra of U0; ::_thesis: the carrier of U1 c= the carrier of U0
 the carrier of U1 is Subset of U0 by UNIALG_2:def_7;
hence  the carrier of U1 c= the carrier of U0 ; ::_thesis: verum
end;

theorem :: UNIALG_3:4
for U0 being Universal_Algebra
for H being non empty Subset of U0
for o being operation of U0 st H is_closed_on o & arity o = 0 holds
o /. H = o
proof
let U0 be Universal_Algebra; ::_thesis: for H being non empty Subset of U0
for o being operation of U0 st H is_closed_on o & arity o = 0 holds
o /. H = o
let H be non empty Subset of U0; ::_thesis: for o being operation of U0 st H is_closed_on o & arity o = 0 holds
o /. H = o
let o be operation of U0; ::_thesis: ( H is_closed_on o & arity o = 0 implies o /. H = o )
assume that
A1: H is_closed_on o and
A2: arity o = 0 ; ::_thesis: o /. H = o
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  o /. H = o by A3, RELAT_1:69; ::_thesis: verum
end;

theorem :: UNIALG_3:5
for U0 being Universal_Algebra holds Constants U0 =  {  (o . {}) where o is operation of U0 : arity o = 0  }
proof
let U0 be Universal_Algebra; ::_thesis: Constants U0 =  {  (o . {}) where o is operation of U0 : arity o = 0  }
set S =  {  (o . {}) where o is operation of U0 : arity o = 0  }  ;
thus  Constants U0 c=  {  (o . {}) where o is operation of U0 : arity o = 0  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (o . {}) where o is operation of U0 : arity o = 0  }  c= Constants U0
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Constants U0 or a in  {  (o . {}) where o is operation of U0 : arity o = 0  }  )
assume  a in Constants U0 ; ::_thesis: a in  {  (o . {}) where o is operation of U0 : arity o = 0  }
then consider u being Element of U0 such that
A1: u = a and
A2: ex o being operation of U0 st
( arity o = 0 & u in rng o ) ;
consider o being operation of U0 such that
A3: arity o = 0 and
A4: u in rng o by A2;
consider a2 being set  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  a in  {  (o . {}) where o is operation of U0 : arity o = 0  }  by A1, A3, A6; ::_thesis: verum
end;
thus   {  (o . {}) where o is operation of U0 : arity o = 0  }  c= Constants U0 ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (o . {}) where o is operation of U0 : arity o = 0  }  or a in Constants U0 )
assume  a in  {  (o . {}) where o is operation of U0 : arity o = 0  }  ; ::_thesis: a in Constants U0
then consider o being 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  a in Constants U0 by A7, A8; ::_thesis: verum
end;
end;

theorem Th6: :: UNIALG_3:6
for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1
proof
let U0 be with_const_op Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1
let U1 be SubAlgebra of U0; ::_thesis: Constants U0 = Constants U1
thus  Constants U0 c= Constants U1 :: according to XBOOLE_0:def_10 ::_thesis: 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Constants U0 or a in Constants U1 )
A1: Constants U0 is Subset of U1 by UNIALG_2:15;
assume A2: a in Constants U0 ; ::_thesis: a in Constants U1
then consider u being Element of U0 such that
A3: u = a and
A4: ex o being operation of U0 st
( arity o = 0 & u in rng o ) ;
consider o1 being 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 being set  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 = 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 by UNIALG_2:def_4;
 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  a in Constants U1 by A2, A3, A5, A6, A1; ::_thesis: verum
end;
thus  Constants U1 c= Constants U0 ::_thesis: verum
proof
reconsider A = the carrier of U1 as non empty Subset of U0 by UNIALG_2:def_7;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Constants U1 or a in Constants U0 )
assume  a in Constants U1 ; ::_thesis: a in Constants U0
then consider u being Element of U1 such that
A11: u = a and
A12: ex o being operation of U1 st
( arity o = 0 & u in rng o ) ;
consider o being operation of U1 such that
A13: arity o = 0 and
A14: u in rng o by A12;
consider x being set  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 = 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 by UNIALG_2:def_1;
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 by UNIALG_2:def_4;
 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  a in Constants U0 by A11, A13, A14, A22; ::_thesis: verum
end;
end;

registration
let U0 be with_const_op Universal_Algebra;
cluster  ->  with_const_op for SubAlgebra of U0;
coherence
 for b1 being SubAlgebra of U0 holds b1 is with_const_op
proof
let U1 be SubAlgebra of U0; ::_thesis: U1 is with_const_op
reconsider U2 = U1 as Universal_Algebra ;
set u = the Element of Constants U2;
 Constants U2 = Constants U0 by Th6;
then  the Element of Constants U2 in Constants U2 ;
then  ex u1 being Element of U2 st
( the Element of Constants U2 = u1 & ex o being operation of U2 st
( arity o = 0 & u1 in rng o ) ) ;
hence  U1 is with_const_op by UNIALG_2:def_11; ::_thesis: verum
end;
end;

theorem :: UNIALG_3:7
for U0 being with_const_op Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2
proof
let U0 be with_const_op Universal_Algebra; ::_thesis: for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2
let U1, U2 be SubAlgebra of U0; ::_thesis: Constants U1 = Constants U2
 Constants U0 = Constants U1 by Th6;
hence  Constants U1 = Constants U2 by Th6; ::_thesis: verum
end;

definition
let U0 be Universal_Algebra;
redefine func Carr U0 means :Def4: :: UNIALG_3:def 4
 for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
it . u = the carrier of U1;
compatibility
 for b1 being Function of (Sub U0),(bool the carrier of U0) holds
( b1 = Carr U0 iff for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
b1 . u = the carrier of U1 )
proof
let f be Function of (Sub U0),(bool the carrier of U0); ::_thesis: ( f = Carr U0 iff for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
f . u = the carrier of U1 )
hereby  ::_thesis: ( ( for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
f . u = the carrier of U1 ) implies f = Carr U0 )
assume A1: f = Carr U0 ; ::_thesis: for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
f . u = the carrier of U1
let u be Element of Sub U0; ::_thesis: for U1 being SubAlgebra of U0 st u = U1 holds
f . u = the carrier of U1
let U1 be SubAlgebra of U0; ::_thesis: ( u = U1 implies f . u = the carrier of U1 )
assume A2: u = U1 ; ::_thesis: f . u = the carrier of U1
 ex U2 being 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; ::_thesis: verum
end;
assume A3: for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
f . u = the carrier of U1 ; ::_thesis: f = Carr U0
 for u1 being Element of Sub U0 holds f . u1 = carr u1
proof
let u be Element of Sub U0; ::_thesis: f . u = carr u
reconsider U1 = u as Element of Sub U0 ;
 f . u = the carrier of U1 by A3;
hence  f . u = carr u by Def2; ::_thesis: verum
end;
hence  f = Carr U0 by Def3; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Carr UNIALG_3:def_4_:_
 for U0 being Universal_Algebra
for b2 being Function of (Sub U0),(bool the carrier of U0) holds
( b2 = Carr U0 iff for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
b2 . u = the carrier of U1 );

theorem :: UNIALG_3:8
for U0 being Universal_Algebra
for H being strict SubAlgebra of U0
for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )
proof
let U0 be Universal_Algebra; ::_thesis: for H being strict SubAlgebra of U0
for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )
let H be strict SubAlgebra of U0; ::_thesis: for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )
let u be Element of U0; ::_thesis: ( u in (Carr U0) . H iff u in H )
thus  ( u in (Carr U0) . H implies u in H ) ::_thesis: ( u in H implies u in (Carr U0) . H )
proof
A1: H in Sub U0 by UNIALG_2:def_14;
assume  u in (Carr U0) . H ; ::_thesis: u in H
then  u in the carrier of H by A1, Def4;
hence  u in H by STRUCT_0:def_5; ::_thesis: verum
end;
thus  ( u in H implies u in (Carr U0) . H ) ::_thesis: verum
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 ; ::_thesis: u in (Carr U0) . H
hence  u in (Carr U0) . H by A2, STRUCT_0:def_5; ::_thesis: verum
end;
end;

theorem Th9: :: UNIALG_3:9
for U0 being Universal_Algebra
for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty
proof
let U0 be Universal_Algebra; ::_thesis: for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty
let H be non empty Subset of (Sub U0); ::_thesis: not (Carr U0) .: H is empty
consider u being 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  not (Carr U0) .: H is empty ; ::_thesis: verum
end;

theorem :: UNIALG_3:10
for U0 being with_const_op Universal_Algebra
for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1
proof
let U0 be with_const_op Universal_Algebra; ::_thesis: for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1
let U1 be strict SubAlgebra of U0; ::_thesis: Constants U0 c= (Carr U0) . U1
 U1 in Sub U0 by Th1;
then A1: (Carr U0) . U1 = the carrier of U1 by Def4;
 Constants U1 = Constants U0 by Th6;
hence  Constants U0 c= (Carr U0) . U1 by A1; ::_thesis: verum
end;

theorem Th11: :: UNIALG_3:11
for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0
for a being set st a is Element of Constants U0 holds
a in the carrier of U1
proof
let U0 be with_const_op Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0
for a being set st a is Element of Constants U0 holds
a in the carrier of U1
let U1 be SubAlgebra of U0; ::_thesis: for a being set st a is Element of Constants U0 holds
a in the carrier of U1
let a be set ; ::_thesis: ( a is Element of Constants U0 implies a in the carrier of U1 )
A1: Constants U0 is Subset of U1 by UNIALG_2:15;
assume  a is Element of Constants U0 ; ::_thesis: a in the carrier of U1
hence  a in the carrier of U1 by A1, TARSKI:def_3; ::_thesis: verum
end;

theorem Th12: :: UNIALG_3:12
for U0 being with_const_op Universal_Algebra
for H being 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; ::_thesis: for H being non empty Subset of (Sub U0) holds meet ((Carr U0) .: H) is non empty Subset of U0
let H be non empty Subset of (Sub U0); ::_thesis: meet ((Carr U0) .: H) is non empty Subset of U0
set u = the Element of Constants U0;
reconsider CH = (Carr U0) .: H as Subset-Family of U0 ;
A1: for S being set st S in (Carr U0) .: H holds
the Element of Constants U0 in S
proof
let S be set ; ::_thesis: ( S in (Carr U0) .: H implies the Element of Constants U0 in S )
assume A2: S in (Carr U0) .: H ; ::_thesis: the Element of Constants U0 in S
then reconsider S = S as Subset of U0 ;
consider X1 being Element of Sub U0 such that
 X1 in H and
A3: S = (Carr U0) . X1 by A2, FUNCT_2:65;
reconsider X1 = X1 as strict SubAlgebra of U0 by UNIALG_2:def_14;
 S = the carrier of X1 by A3, Def4;
hence  the Element of Constants U0 in S by Th11; ::_thesis: verum
end;
 CH <> {} by Th9;
hence  meet ((Carr U0) .: H) is non empty Subset of U0 by A1, SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: UNIALG_3:13
for U0 being with_const_op Universal_Algebra holds the carrier of (UnSubAlLattice U0) = Sub U0 ;

theorem Th14: :: UNIALG_3:14
for U0 being with_const_op Universal_Algebra
for H being non empty Subset of (Sub U0)
for S being 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; ::_thesis: for H being non empty Subset of (Sub U0)
for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds
S is opers_closed
let H be non empty Subset of (Sub U0); ::_thesis: for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds
S is opers_closed
let S be non empty Subset of U0; ::_thesis: ( S = meet ((Carr U0) .: H) implies S is opers_closed )
assume A1: S = meet ((Carr U0) .: H) ; ::_thesis: S is opers_closed
A2: (Carr U0) .: H <> {} by Th9;
 for o being operation of U0 holds S is_closed_on o
proof
let o be operation of U0; ::_thesis: S is_closed_on o
let s be FinSequence of S; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in S )
assume A3: len s = arity o ; ::_thesis: o . s in S
now__::_thesis:_for_a_being_set_st_a_in_(Carr_U0)_.:_H_holds_
o_._s_in_a
let a be set ; ::_thesis: ( a in (Carr U0) .: H implies o . s in a )
assume A4: a in (Carr U0) .: H ; ::_thesis: o . s in a
then reconsider H1 = a as Subset of U0 ;
consider H2 being 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 by UNIALG_2:def_4;
then  o . s1 in H3 by A3, UNIALG_2:def_3;
hence  o . s in a ; ::_thesis: verum
end;
hence  o . s in S by A1, A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence  S is opers_closed by UNIALG_2:def_4; ::_thesis: verum
end;

definition
let U0 be strict with_const_op Universal_Algebra;
let H be non empty Subset of (Sub U0);
func meet H ->  strict SubAlgebra of U0 means :Def5: :: UNIALG_3:def 5
 the carrier of it = meet ((Carr U0) .: H);
existence
 ex b1 being strict SubAlgebra of U0 st the carrier of b1 = meet ((Carr U0) .: H)
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  ex b1 being strict SubAlgebra of U0 st the carrier of b1 = meet ((Carr U0) .: H) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SubAlgebra of U0 st the carrier of b1 = meet ((Carr U0) .: H) & the carrier of b2 = meet ((Carr U0) .: H) holds
b1 = b2 by UNIALG_2:12;
end;

:: deftheorem Def5 defines meet UNIALG_3:def_5_:_
 for U0 being strict with_const_op Universal_Algebra
for H being non empty Subset of (Sub U0)
for b3 being strict SubAlgebra of U0 holds
( b3 = meet H iff the carrier of b3 = meet ((Carr U0) .: H) );

theorem Th15: :: UNIALG_3:15
for U0 being with_const_op Universal_Algebra
for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being 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; ::_thesis: for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )
let l1, l2 be Element of (UnSubAlLattice U0); ::_thesis: for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )
let U1, U2 be strict SubAlgebra of U0; ::_thesis: ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff the carrier of U1 c= the carrier of U2 ) )
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 ; ::_thesis: the carrier of U1 c= the carrier of U2
then  l1 "\/" l2 = l2 by LATTICES:def_3;
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, XBOOLE_0:def_10;
hence  the carrier of U1 c= the carrier of U2 by XBOOLE_1:7; ::_thesis: verum
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 ; ::_thesis: l1 [= l2
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  l1 [= l2 by LATTICES:def_3; ::_thesis: verum
end;
hence  ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff the carrier of U1 c= the carrier of U2 ) ) by A1; ::_thesis: verum
end;

theorem :: UNIALG_3:16
for U0 being with_const_op Universal_Algebra
for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being 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; ::_thesis: for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff U1 is SubAlgebra of U2 )
let l1, l2 be Element of (UnSubAlLattice U0); ::_thesis: for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff U1 is SubAlgebra of U2 )
let U1, U2 be strict SubAlgebra of U0; ::_thesis: ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff U1 is SubAlgebra of U2 ) )
assume A1: ( l1 = U1 & l2 = U2 ) ; ::_thesis: ( l1 [= l2 iff U1 is SubAlgebra of U2 )
thus  ( l1 [= l2 implies U1 is SubAlgebra of U2 ) ::_thesis: ( U1 is SubAlgebra of U2 implies l1 [= l2 )
proof
assume  l1 [= l2 ; ::_thesis: U1 is SubAlgebra of U2
then  the carrier of U1 c= the carrier of U2 by A1, Th15;
hence  U1 is SubAlgebra of U2 by UNIALG_2:11; ::_thesis: verum
end;
thus  ( U1 is SubAlgebra of U2 implies l1 [= l2 ) ::_thesis: verum
proof
assume  U1 is SubAlgebra of U2 ; ::_thesis: l1 [= l2
then  the carrier of U1 is Subset of U2 by UNIALG_2:def_7;
hence  l1 [= l2 by A1, Th15; ::_thesis: verum
end;
end;

theorem Th17: :: UNIALG_3:17
for U0 being strict with_const_op Universal_Algebra holds UnSubAlLattice U0 is bounded
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: UnSubAlLattice U0 is bounded
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 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( l1 "/\" b1 = l1 & b1 "/\" l1 = l1 )
let l2 be Element of (UnSubAlLattice U0); ::_thesis: ( l1 "/\" l2 = l1 & l2 "/\" l1 = l1 )
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 by LATTICES:5;
hence  l1 "/\" l2 = l1 by LATTICES:4; ::_thesis: l2 "/\" l1 = l1
thus  l2 "/\" l1 = l1 by A2, LATTICES:4; ::_thesis: verum
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 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( l1 "\/" b1 = l1 & b1 "\/" l1 = l1 )
let l2 be Element of (UnSubAlLattice U0); ::_thesis: ( l1 "\/" l2 = l1 & l2 "\/" l1 = l1 )
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 ; ::_thesis: l2 "\/" l1 = l1
hence  l2 "\/" l1 = l1 ; ::_thesis: verum
end;
hence  UnSubAlLattice U0 is bounded by A1; ::_thesis: verum
end;

registration
let U0 be strict with_const_op Universal_Algebra;
cluster UnSubAlLattice U0 ->  bounded ;
coherence
 UnSubAlLattice U0 is bounded by Th17;
end;

theorem Th18: :: UNIALG_3:18
for U0 being strict with_const_op Universal_Algebra
for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)
let U1 be strict SubAlgebra of U0; ::_thesis: (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)
set C = Constants U0;
set G = GenUnivAlg (Constants U0);
 Constants U0 is Subset of U1 by UNIALG_2:15;
then  GenUnivAlg (Constants U0) is strict SubAlgebra of U1 by UNIALG_2:def_12;
then A1: the carrier of (GenUnivAlg (Constants U0)) is Subset of U1 by UNIALG_2:def_7;
 the carrier of (GenUnivAlg (Constants U0)) meets the carrier of U1 by UNIALG_2:17;
then  the carrier of ((GenUnivAlg (Constants U0)) /\ U1) = the carrier of (GenUnivAlg (Constants U0)) /\ the carrier of U1 by UNIALG_2:def_9;
hence  (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0) by A1, UNIALG_2:12, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: UNIALG_3:19
for U0 being strict with_const_op Universal_Algebra holds Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)
set L = UnSubAlLattice U0;
set C = Constants U0;
reconsider G = GenUnivAlg (Constants U0) as Element of Sub U0 by UNIALG_2:def_14;
reconsider l1 = G as Element of (UnSubAlLattice U0) ;
now__::_thesis:_for_l_being_Element_of_(UnSubAlLattice_U0)_holds_
(_l1_"/\"_l_=_l1_&_l_"/\"_l1_=_l1_)
let l be Element of (UnSubAlLattice U0); ::_thesis: ( l1 "/\" l = l1 & l "/\" l1 = l1 )
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 (Constants U0)) /\ U2 by UNIALG_2:def_16
.= l1 by Th18 ; ::_thesis: l "/\" l1 = l1
hence  l "/\" l1 = l1 ; ::_thesis: verum
end;
hence  Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0) by LATTICES:def_16; ::_thesis: verum
end;

theorem Th20: :: UNIALG_3:20
for U0 being strict with_const_op Universal_Algebra
for U1 being SubAlgebra of U0
for H being Subset of U0 st H = the carrier of U0 holds
(GenUnivAlg H) "\/" U1 = GenUnivAlg H
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: for U1 being SubAlgebra of U0
for H being Subset of U0 st H = the carrier of U0 holds
(GenUnivAlg H) "\/" U1 = GenUnivAlg H
let U1 be SubAlgebra of U0; ::_thesis: for H being Subset of U0 st H = the carrier of U0 holds
(GenUnivAlg H) "\/" U1 = GenUnivAlg H
let H be Subset of U0; ::_thesis: ( H = the carrier of U0 implies (GenUnivAlg H) "\/" U1 = GenUnivAlg H )
assume  H = the carrier of U0 ; ::_thesis: (GenUnivAlg H) "\/" U1 = GenUnivAlg H
then  H \/ the carrier of U1 = H by Th3, XBOOLE_1:12;
hence  (GenUnivAlg H) "\/" U1 = GenUnivAlg H by UNIALG_2:20; ::_thesis: verum
end;

theorem Th21: :: UNIALG_3:21
for U0 being strict with_const_op Universal_Algebra
for H being Subset of U0 st H = the carrier of U0 holds
Top (UnSubAlLattice U0) = GenUnivAlg H
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: for H being Subset of U0 st H = the carrier of U0 holds
Top (UnSubAlLattice U0) = GenUnivAlg H
let H be Subset of U0; ::_thesis: ( H = the carrier of U0 implies Top (UnSubAlLattice U0) = GenUnivAlg H )
set L = UnSubAlLattice U0;
reconsider u1 = GenUnivAlg H as Element of Sub U0 by UNIALG_2:def_14;
reconsider l1 = u1 as Element of (UnSubAlLattice U0) ;
assume A1: H = the carrier of U0 ; ::_thesis: Top (UnSubAlLattice U0) = GenUnivAlg H
now__::_thesis:_for_l_being_Element_of_(UnSubAlLattice_U0)_holds_
(_l1_"\/"_l_=_l1_&_l_"\/"_l1_=_l1_)
let l be Element of (UnSubAlLattice U0); ::_thesis: ( l1 "\/" l = l1 & l "\/" l1 = l1 )
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 ; ::_thesis: l "\/" l1 = l1
hence  l "\/" l1 = l1 ; ::_thesis: verum
end;
hence  Top (UnSubAlLattice U0) = GenUnivAlg H by LATTICES:def_17; ::_thesis: verum
end;

theorem :: UNIALG_3:22
for U0 being strict with_const_op Universal_Algebra holds Top (UnSubAlLattice U0) = U0
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: Top (UnSubAlLattice U0) = U0
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 ; ::_thesis: verum
end;

theorem :: UNIALG_3:23
for U0 being strict with_const_op Universal_Algebra holds UnSubAlLattice U0 is complete
proof
let U0 be strict with_const_op Universal_Algebra; ::_thesis: UnSubAlLattice U0 is complete
let L be Subset of (UnSubAlLattice U0); :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of (UnSubAlLattice U0) st
( b1 is_less_than L & ( for b2 being Element of the carrier of (UnSubAlLattice U0) holds
( not b2 is_less_than L or b2 [= b1 ) ) )
percases ( L = {} or L <> {} ) ;
supposeA1: L = {} ; ::_thesis: ex b1 being Element of the carrier of (UnSubAlLattice U0) st
( b1 is_less_than L & ( for b2 being Element of the carrier of (UnSubAlLattice U0) holds
( not b2 is_less_than L or b2 [= b1 ) ) )
thus  ex b1 being Element of the carrier of (UnSubAlLattice U0) st
( b1 is_less_than L & ( for b2 being Element of the carrier of (UnSubAlLattice U0) holds
( not b2 is_less_than L or b2 [= b1 ) ) ) ::_thesis: verum
proof
take  Top (UnSubAlLattice U0) ; ::_thesis: ( Top (UnSubAlLattice U0) is_less_than L & ( for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( not b1 is_less_than L or b1 [= Top (UnSubAlLattice U0) ) ) )
thus  Top (UnSubAlLattice U0) is_less_than L ::_thesis: for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( not b1 is_less_than L or b1 [= Top (UnSubAlLattice U0) )
proof
let l1 be Element of (UnSubAlLattice U0); :: according to LATTICE3:def_16 ::_thesis: ( not l1 in L or Top (UnSubAlLattice U0) [= l1 )
thus  ( not l1 in L or Top (UnSubAlLattice U0) [= l1 ) by A1; ::_thesis: verum
end;
let l2 be Element of (UnSubAlLattice U0); ::_thesis: ( not l2 is_less_than L or l2 [= Top (UnSubAlLattice U0) )
assume  l2 is_less_than L ; ::_thesis: l2 [= Top (UnSubAlLattice U0)
thus  l2 [= Top (UnSubAlLattice U0) by LATTICES:19; ::_thesis: verum
end;
end;
suppose L <> {} ; ::_thesis: ex b1 being Element of the carrier of (UnSubAlLattice U0) st
( b1 is_less_than L & ( for b2 being Element of the carrier of (UnSubAlLattice U0) holds
( not b2 is_less_than L or b2 [= b1 ) ) )
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 ; ::_thesis: ( l1 is_less_than L & ( for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( not b1 is_less_than L or b1 [= l1 ) ) )
set x = the Element of H;
thus  l1 is_less_than L ::_thesis: for b1 being Element of the carrier of (UnSubAlLattice U0) holds
( not b1 is_less_than L or b1 [= l1 )
proof
let l2 be Element of (UnSubAlLattice U0); :: according to LATTICE3:def_16 ::_thesis: ( not l2 in L or l1 [= l2 )
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 ; ::_thesis: l1 [= l2
 (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; ::_thesis: verum
end;
let l3 be Element of (UnSubAlLattice U0); ::_thesis: ( not l3 is_less_than L or l3 [= l1 )
reconsider U1 = l3 as strict SubAlgebra of U0 by UNIALG_2:def_14;
assume A3: l3 is_less_than L ; ::_thesis: l3 [= l1
A4: for A being set st A in (Carr U0) .: H holds
the carrier of U1 c= A
proof
let A be set ; ::_thesis: ( A in (Carr U0) .: H implies the carrier of U1 c= A )
assume A5: A in (Carr U0) .: H ; ::_thesis: the carrier of U1 c= A
then reconsider H1 = A as Subset of U0 ;
consider l4 being Element of Sub U0 such that
A6: ( l4 in H & H1 = (Carr U0) . l4 ) by A5, FUNCT_2:65;
reconsider l4 = 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, LATTICE3:def_16;
hence  the carrier of U1 c= A by Th15; ::_thesis: verum
end;
 (Carr U0) . the Element of H 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; ::_thesis: verum
end;
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;
func FuncLatt F ->  Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) means :Def6: :: UNIALG_3:def 6
 for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
it . U1 = GenUnivAlg H;
existence
 ex b1 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) st
for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
b1 . U1 = GenUnivAlg H
proof
defpred S1[ set , set ] means  for U1 being strict SubAlgebra of U01 st U1 = $1 holds
for S being Subset of U02 st S = F .: the carrier of U1 holds
$2 = GenUnivAlg (F .: the carrier of U1);
A1: for u1 being set st u1 in the carrier of (UnSubAlLattice U01) holds
ex u2 being set st
( u2 in the carrier of (UnSubAlLattice U02) & S1[u1,u2] )
proof
let u1 be set ; ::_thesis: ( u1 in the carrier of (UnSubAlLattice U01) implies ex u2 being set st
( u2 in the carrier of (UnSubAlLattice U02) & S1[u1,u2] ) )
assume  u1 in the carrier of (UnSubAlLattice U01) ; ::_thesis: ex u2 being set st
( u2 in the carrier of (UnSubAlLattice U02) & S1[u1,u2] )
then consider U2 being 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 = u2 as Element of (UnSubAlLattice U02) by UNIALG_2:def_14;
take  u2 ; ::_thesis: ( u2 in the carrier of (UnSubAlLattice U02) & S1[u1,u2] )
thus  ( u2 in the carrier of (UnSubAlLattice U02) & S1[u1,u2] ) by A2; ::_thesis: verum
end;
consider f1 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) such that
A3: for u1 being set st u1 in the carrier of (UnSubAlLattice U01) holds
S1[u1,f1 . u1] from FUNCT_2:sch_1(A1);
take  f1 ; ::_thesis: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H
thus  for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H ::_thesis: verum
proof
let U1 be strict SubAlgebra of U01; ::_thesis: for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H
let S be Subset of U02; ::_thesis: ( S = F .: the carrier of U1 implies f1 . U1 = GenUnivAlg S )
A4: U1 is Element of Sub U01 by UNIALG_2:def_14;
assume  S = F .: the carrier of U1 ; ::_thesis: f1 . U1 = GenUnivAlg S
hence  f1 . U1 = GenUnivAlg S by A3, A4; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) st ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
b1 . U1 = GenUnivAlg H ) & ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
b2 . U1 = GenUnivAlg H ) holds
b1 = b2
proof
let F1, F2 be Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02); ::_thesis: ( ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F1 . U1 = GenUnivAlg H ) & ( for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F2 . U1 = GenUnivAlg H ) implies F1 = F2 )
assume that
A5: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F1 . U1 = GenUnivAlg H and
A6: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
F2 . U1 = GenUnivAlg H ; ::_thesis: F1 = F2
 for l being set st l in the carrier of (UnSubAlLattice U01) holds
F1 . l = F2 . l
proof
let l be set ; ::_thesis: ( l in the carrier of (UnSubAlLattice U01) implies F1 . l = F2 . l )
assume  l in the carrier of (UnSubAlLattice U01) ; ::_thesis: F1 . l = F2 . l
then consider U1 being strict SubAlgebra of U01 such that
A7: U1 = l by Th1;
consider H being Subset of U02 such that
A8: H = F .: the carrier of U1 ;
 F1 . l = GenUnivAlg H by A5, A7, A8;
hence  F1 . l = F2 . l by A6, A7, A8; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines FuncLatt UNIALG_3:def_6_:_
 for U01, U02 being with_const_op Universal_Algebra
for F being Function of the carrier of U01, the carrier of U02
for b4 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) holds
( b4 = FuncLatt F iff for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
b4 . U1 = GenUnivAlg H );

theorem :: UNIALG_3:24
for U0 being strict with_const_op Universal_Algebra
for F being 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 strict with_const_op Universal_Algebra; ::_thesis: for F being 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)
let F be Function of the carrier of U0, the carrier of U0; ::_thesis: ( F = id the carrier of U0 implies FuncLatt F = id the carrier of (UnSubAlLattice U0) )
assume A1: F = id the carrier of U0 ; ::_thesis: FuncLatt F = id the carrier of (UnSubAlLattice U0)
A2: for a being set st a in the carrier of (UnSubAlLattice U0) holds
(FuncLatt F) . a = a
proof
let a be set ; ::_thesis: ( a in the carrier of (UnSubAlLattice U0) implies (FuncLatt F) . a = a )
assume  a in the carrier of (UnSubAlLattice U0) ; ::_thesis: (FuncLatt F) . a = a
then reconsider a = a as strict SubAlgebra of U0 by UNIALG_2:def_14;
 for a1 being set st a1 in the carrier of a holds
a1 in F .: the carrier of a
proof
let a1 be set ; ::_thesis: ( a1 in the carrier of a implies a1 in F .: the carrier of a )
assume A3: a1 in the carrier of a ; ::_thesis: a1 in F .: the carrier of a
 the carrier of a c= the carrier of U0 by Th3;
then reconsider a1 = a1 as Element of U0 by A3;
 F . a1 = a1 by A1, FUNCT_1:17;
hence  a1 in F .: the carrier of a by A3, FUNCT_2:35; ::_thesis: verum
end;
then A4: the carrier of a c= F .: the carrier of a by TARSKI:def_3;
 for a1 being set st a1 in F .: the carrier of a holds
a1 in the carrier of a
proof
let a1 be set ; ::_thesis: ( a1 in F .: the carrier of a implies a1 in the carrier of a )
assume A5: a1 in F .: the carrier of a ; ::_thesis: a1 in the carrier of a
then reconsider a1 = a1 as Element of U0 ;
 ex H being Element of U0 st
( H in the carrier of a & a1 = F . H ) by A5, FUNCT_2:65;
hence  a1 in the carrier of a by A1, FUNCT_1:17; ::_thesis: verum
end;
then A6: F .: the carrier of a c= the carrier of a by TARSKI:def_3;
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, XBOOLE_0:def_10;
then  (FuncLatt F) . a = GenUnivAlg H1 by Def6;
hence  (FuncLatt F) . a = a by UNIALG_2:19; ::_thesis: verum
end;
 dom (FuncLatt F) = the carrier of (UnSubAlLattice U0) by FUNCT_2:def_1;
hence  FuncLatt F = id the carrier of (UnSubAlLattice U0) by A2, FUNCT_1:17; ::_thesis: verum
end;