:: SUBSTLAT semantic presentation

begin


definition
let V, C be set ;
func SubstitutionSet (V,C) ->  Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1
 {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ;
coherence
  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  is Subset of (Fin (PFuncs (V,C)))
proof
set IT =  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ;
  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  c= Fin (PFuncs (V,C))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  or x in Fin (PFuncs (V,C)) )
assume  x in  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ; ::_thesis: x in Fin (PFuncs (V,C))
then  ex B being Element of Fin (PFuncs (V,C)) st
( B = x & ( for u being set st u in B holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds
s = t ) ) ;
hence  x in Fin (PFuncs (V,C)) ; ::_thesis: verum
end;
hence   {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  is Subset of (Fin (PFuncs (V,C))) ; ::_thesis: verum
end;
end;

:: deftheorem  defines SubstitutionSet SUBSTLAT:def_1_:_
 for V, C being set holds SubstitutionSet (V,C) =  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ;

Lm1:  for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite
proof
let V, C be set ; ::_thesis: for a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite
let a, b be set ; ::_thesis: ( b in SubstitutionSet (V,C) & a in b implies a is finite )
assume that
A1: b in SubstitutionSet (V,C) and
A2: a in b ; ::_thesis: a is finite
 ex A being Element of Fin (PFuncs (V,C)) st
( A = b & ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) by A1;
hence  a is finite by A2; ::_thesis: verum
end;

theorem Th1: :: SUBSTLAT:1
for V, C being set holds {} in SubstitutionSet (V,C)
proof
let V, C be set ; ::_thesis: {} in SubstitutionSet (V,C)
 {} c= PFuncs (V,C) by XBOOLE_1:2;
then A1: {} in Fin (PFuncs (V,C)) by FINSUB_1:def_5;
 ( ( for u being set st u in {} holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in {} & t in {} & s c= t holds
s = t ) ) ;
hence  {} in SubstitutionSet (V,C) by A1; ::_thesis: verum
end;

theorem Th2: :: SUBSTLAT:2
for V, C being set holds {{}} in SubstitutionSet (V,C)
proof
let V, C be set ; ::_thesis: {{}} in SubstitutionSet (V,C)
A1: for s, t being Element of PFuncs (V,C) st s in {{}} & t in {{}} & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in {{}} & t in {{}} & s c= t implies s = t )
assume that
A2: s in {{}} and
A3: t in {{}} and
 s c= t ; ::_thesis: s = t
 s = {} by A2, TARSKI:def_1;
hence  s = t by A3, TARSKI:def_1; ::_thesis: verum
end;
 {} is PartFunc of V,C by RELSET_1:12;
then  {} in PFuncs (V,C) by PARTFUN1:45;
then  {{}} c= PFuncs (V,C) by ZFMISC_1:31;
then A4: {{}} in Fin (PFuncs (V,C)) by FINSUB_1:def_5;
 for u being set st u in {{}} holds
u is finite ;
hence  {{}} in SubstitutionSet (V,C) by A4, A1; ::_thesis: verum
end;

registration
let V, C be set ;
cluster SubstitutionSet (V,C) ->  non empty ;
coherence
 not SubstitutionSet (V,C) is empty by Th2;
end;

definition
let V, C be set ;
let A, B be Element of SubstitutionSet (V,C);
:: original: \/
redefine funcA \/ B ->  Element of Fin (PFuncs (V,C));
coherence
 A \/ B is Element of Fin (PFuncs (V,C))
proof
 A \/ B in Fin (PFuncs (V,C)) ;
hence  A \/ B is Element of Fin (PFuncs (V,C)) ; ::_thesis: verum
end;
end;

registration
let V, C be set ;
cluster non empty for Element of SubstitutionSet (V,C);
existence
 not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty
proof
 {{}} in SubstitutionSet (V,C) by Th2;
hence  not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty ; ::_thesis: verum
end;
end;

registration
let V, C be set ;
cluster  ->  finite for Element of SubstitutionSet (V,C);
coherence
 for b1 being Element of SubstitutionSet (V,C) holds b1 is finite ;
end;

definition
let V, C be set ;
let A be Element of Fin (PFuncs (V,C));
func mi A ->  Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2
 {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ;
coherence
  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  is Element of SubstitutionSet (V,C)
proof
set M =  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ;
A1:  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  c= PFuncs (V,C)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  or a in PFuncs (V,C) )
assume  a in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ; ::_thesis: a in PFuncs (V,C)
then  ex t9 being Element of PFuncs (V,C) st
( a = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence  a in PFuncs (V,C) ; ::_thesis: verum
end;
A2: now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_PFuncs_(V,C)_:_(_t_is_finite_&_(_for_s_being_Element_of_PFuncs_(V,C)_holds_
(_(_s_in_A_&_s_c=_t_)_iff_s_=_t_)_)_)__}__holds_
x_in_A
let x be set ; ::_thesis: ( x in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  implies x in A )
assume  x in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ; ::_thesis: x in A
then  ex t being Element of PFuncs (V,C) st
( x = t & t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) ;
hence  x in A ; ::_thesis: verum
end;
then A3:  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  c= A by TARSKI:def_3;
reconsider M =  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  as set ;
reconsider M9 = M as Element of Fin (PFuncs (V,C)) by A1, A3, FINSUB_1:def_5;
A4: for u being set st u in M9 holds
u is finite
proof
let u be set ; ::_thesis: ( u in M9 implies u is finite )
assume  u in M9 ; ::_thesis: u is finite
then  ex t9 being Element of PFuncs (V,C) st
( u = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence  u is finite ; ::_thesis: verum
end;
 for s, t being Element of PFuncs (V,C) st s in M9 & t in M9 & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in M9 & t in M9 & s c= t implies s = t )
assume that
A5: ( s in M9 & t in M9 ) and
A6: s c= t ; ::_thesis: s = t
 ( s in A & ex tt being Element of PFuncs (V,C) st
( t = tt & tt is finite & ( for ss being Element of PFuncs (V,C) holds
( ( ss in A & ss c= tt ) iff ss = tt ) ) ) ) by A2, A5;
hence  s = t by A6; ::_thesis: verum
end;
then  M in  {  A1 where A1 is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A1 holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds
s = t ) )  }  by A4;
hence   {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  is Element of SubstitutionSet (V,C) ; ::_thesis: verum
end;
end;

:: deftheorem  defines mi SUBSTLAT:def_2_:_
 for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A =  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ;

registration
let V, C be set ;
cluster  ->  functional for Element of SubstitutionSet (V,C);
coherence
 for b1 being Element of SubstitutionSet (V,C) holds b1 is functional
proof
let A be Element of SubstitutionSet (V,C); ::_thesis: A is functional
 A c= PFuncs (V,C) by FINSUB_1:def_5;
hence  A is functional ; ::_thesis: verum
end;
end;

definition
let V, C be set ;
let A, B be Element of Fin (PFuncs (V,C));
funcA ^ B ->  Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3
 {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ;
coherence
  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  is Element of Fin (PFuncs (V,C))
proof
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) ->  set = $1 \/ $2;
set M =  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ;
set N =  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }  ;
A1:  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  c=  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  or a in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }  )
assume  a in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ; ::_thesis: a in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }
then  ex s, t being Element of PFuncs (V,C) st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence  a in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }  ; ::_thesis: verum
end;
A2:  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  c= PFuncs (V,C)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  or y in PFuncs (V,C) )
assume  y in  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ; ::_thesis: y in PFuncs (V,C)
then consider s, t being Element of PFuncs (V,C) such that
A3: y = s \/ t and
 s in A and
 t in B and
A4: s tolerates t ;
reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47;
reconsider s9 = s, t9 = t as Function ;
 ( s is PartFunc of V,C & t is PartFunc of V,C ) by PARTFUN1:47;
then  s9 +* t9 is PartFunc of V,C by FUNCT_4:40;
then  s99 \/ t99 is PartFunc of V,C by A4, FUNCT_4:30;
hence  y in PFuncs (V,C) by A3, PARTFUN1:45; ::_thesis: verum
end;
A5: B is finite ;
A6: A is finite ;
  {  H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B )  }  is finite from FRAENKEL:sch_22(A6, A5);
hence   {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem  defines ^ SUBSTLAT:def_3_:_
 for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B =  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ;


theorem Th3: :: SUBSTLAT:3
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: A ^ B = B ^ A
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) ->  set = $1 \/ $2;
defpred S1[ Function, Function] means ( $1 in A & $2 in B & $1 tolerates $2 );
defpred S2[ Function, Function] means ( $2 in B & $1 in A & $2 tolerates $1 );
set X1 =  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t]  }  ;
set X2 =  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  ;
A1: now__::_thesis:_for_x_being_set_holds_
(_x_in__{__H1(t,s)_where_s,_t_is_Element_of_PFuncs_(V,C)_:_S2[s,t]__}__iff_x_in__{__(t_\/_s)_where_t,_s_is_Element_of_PFuncs_(V,C)_:_(_t_in_B_&_s_in_A_&_t_tolerates_s_)__}__)
let x be set ; ::_thesis: ( x in  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  iff x in  {  (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s )  }  )
 ( x in  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  iff ex s, t being Element of PFuncs (V,C) st
( x = H1(t,s) & S2[s,t] ) ) ;
then  ( x in  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  iff ex t, s being Element of PFuncs (V,C) st
( x = t \/ s & t in B & s in A & t tolerates s ) ) ;
hence  ( x in  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  iff x in  {  (t \/ s) where t, s is Element of PFuncs (V,C) : ( t in B & s in A & t tolerates s )  }  ) ; ::_thesis: verum
end;
A2: for s, t being Element of PFuncs (V,C) holds H1(s,t) = H1(t,s) ;
A3: for s, t being Element of PFuncs (V,C) holds
( S1[s,t] iff S2[s,t] ) ;
  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t]  }  =  {  H1(t,s) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  from FRAENKEL:sch_8(A3, A2);
hence  A ^ B = B ^ A by A1, TARSKI:1; ::_thesis: verum
end;

theorem Th4: :: SUBSTLAT:4
for V, C being set
for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
proof
let V, C be set ; ::_thesis: for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
let B, A be Element of Fin (PFuncs (V,C)); ::_thesis: ( B = {{}} implies A ^ B = A )
A1:  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }  c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }  or a in A )
assume  a in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }  ; ::_thesis: a in A
then consider s9, t9 being Element of PFuncs (V,C) such that
A2: ( a = s9 \/ t9 & s9 in A ) and
A3: t9 in {{}} and
 s9 tolerates t9 ;
 t9 = {} by A3, TARSKI:def_1;
hence  a in A by A2; ::_thesis: verum
end;
A4: A c=  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }
proof
 {} is PartFunc of V,C by RELSET_1:12;
then reconsider b = {} as Element of PFuncs (V,C) by PARTFUN1:45;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }  )
assume A5: a in A ; ::_thesis: a in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }
 A c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A5;
A6: b in {{}} by TARSKI:def_1;
 ( a = a9 \/ b & a9 tolerates b ) by PARTFUN1:59;
hence  a in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t )  }  by A5, A6; ::_thesis: verum
end;
assume  B = {{}} ; ::_thesis: A ^ B = A
hence  A ^ B = A by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th5: :: SUBSTLAT:5
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
let a, b be set ; ::_thesis: ( B in SubstitutionSet (V,C) & a in B & b in B & a c= b implies a = b )
assume  B in SubstitutionSet (V,C) ; ::_thesis: ( not a in B or not b in B or not a c= b or a = b )
then A1: ex A1 being Element of Fin (PFuncs (V,C)) st
( A1 = B & ( for u being set st u in A1 holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A1 & t in A1 & s c= t holds
s = t ) ) ;
assume that
A2: ( a in B & b in B ) and
A3: a c= b ; ::_thesis: a = b
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V,C) by A2;
 a9 = b9 by A1, A2, A3;
hence  a = b ; ::_thesis: verum
end;

theorem Th6: :: SUBSTLAT:6
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
let a be set ; ::_thesis: ( a in mi B implies ( a in B & ( for b being set st b in B & b c= a holds
b = a ) ) )
assume  a in mi B ; ::_thesis: ( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
then A1: ex t being Element of PFuncs (V,C) st
( a = t & t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence  a in B ; ::_thesis: for b being set st b in B & b c= a holds
b = a
let b be set ; ::_thesis: ( b in B & b c= a implies b = a )
assume that
A2: b in B and
A3: b c= a ; ::_thesis: b = a
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A2;
 b9 = a by A1, A2, A3;
hence  b = a ; ::_thesis: verum
end;

Lm2:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: ( ( for a being set st a in A holds
a in B ) implies A c= B )
assume A1: for a being set st a in A holds
a in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
hence  x in B by A1; ::_thesis: verum
end;

registration
let V, C be set ;
clusterV1() Function-like finite for Element of PFuncs (V,C);
existence
 ex b1 being Element of PFuncs (V,C) st b1 is finite
proof
 {} is PartFunc of V,C by RELSET_1:12;
then reconsider e = {} as Element of PFuncs (V,C) by PARTFUN1:45;
take  e ; ::_thesis: e is finite
thus  e is finite ; ::_thesis: verum
end;
end;

theorem Th7: :: SUBSTLAT:7
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let a be finite set ; ::_thesis: ( a in B & ( for b being finite set st b in B & b c= a holds
b = a ) implies a in mi B )
assume that
A1: a in B and
A2: for s being finite set st s in B & s c= a holds
s = a ; ::_thesis: a in mi B
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
 for s being Element of PFuncs (V,C) holds
( ( s in B & s c= a ) iff s = a ) by A1, A2;
then  a9 in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in B & s c= t ) iff s = t ) ) )  }  ;
hence  a in mi B ; ::_thesis: verum
end;

theorem Th8: :: SUBSTLAT:8
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
proof
let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi A c= A
 for a being set st a in mi A holds
a in A by Th6;
hence  mi A c= A by TARSKI:def_3; ::_thesis: verum
end;

theorem :: SUBSTLAT:9
for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by Th8, XBOOLE_1:3;

theorem Th10: :: SUBSTLAT:10
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
let B be Element of Fin (PFuncs (V,C)); ::_thesis: for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
defpred S1[ set , set ] means $1 c= $2;
let b be finite set ; ::_thesis: ( b in B implies ex c being set st
( c c= b & c in mi B ) )
assume A1: b in B ; ::_thesis: ex c being set st
( c c= b & c in mi B )
A2: B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A1;
A3: for a, b, c being Element of PFuncs (V,C) st S1[a,b] & S1[b,c] holds
S1[a,c] by XBOOLE_1:1;
A4: for a being Element of PFuncs (V,C) holds S1[a,a] ;
 for a being Element of PFuncs (V,C) st a in B holds
ex b being Element of PFuncs (V,C) st
( b in B & S1[b,a] & ( for c being Element of PFuncs (V,C) st c in B & S1[c,b] holds
S1[b,c] ) ) from FRAENKEL:sch_23(A4, A3);
then consider c being Element of PFuncs (V,C) such that
A5: c in B and
A6: c c= b9 and
A7: for a being Element of PFuncs (V,C) st a in B & a c= c holds
c c= a by A1;
take  c ; ::_thesis: ( c c= b & c in mi B )
thus  c c= b by A6; ::_thesis: c in mi B
now__::_thesis:_for_b_being_finite_set_st_b_in_B_&_b_c=_c_holds_
b_=_c
let b be finite set ; ::_thesis: ( b in B & b c= c implies b = c )
assume that
A8: b in B and
A9: b c= c ; ::_thesis: b = c
reconsider b9 = b as Element of PFuncs (V,C) by A2, A8;
 c c= b9 by A7, A8, A9;
hence  b = c by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  c in mi B by A5, A6, Th7; ::_thesis: verum
end;

theorem Th11: :: SUBSTLAT:11
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi K = K
proof
let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi K = K
let K be Element of SubstitutionSet (V,C); ::_thesis: mi K = K
thus  mi K c= K by Th8; :: according to XBOOLE_0:def_10 ::_thesis: K c= mi K
now__::_thesis:_for_a_being_set_st_a_in_K_holds_
a_in_mi_K
let a be set ; ::_thesis: ( a in K implies a in mi K )
assume A1: a in K ; ::_thesis: a in mi K
then  ( a is finite & ( for b being finite set st b in K & b c= a holds
b = a ) ) by Lm1, Th5;
hence  a in mi K by A1, Th7; ::_thesis: verum
end;
hence  K c= mi K by Lm2; ::_thesis: verum
end;

theorem Th12: :: SUBSTLAT:12
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A \/ B) c= (mi A) \/ B
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_
a_in_(mi_A)_\/_B
let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in (mi A) \/ B )
assume A1: a in mi (A \/ B) ; ::_thesis: a in (mi A) \/ B
then reconsider a9 = a as finite set by Lm1;
A2: a in A \/ B by A1, Th6;
now__::_thesis:_a_in_(mi_A)_\/_B
percases ( a in A or a in B ) by A2, XBOOLE_0:def_3;
supposeA3: a in A ; ::_thesis: a in (mi A) \/ B
now__::_thesis:_for_b_being_finite_set_st_b_in_A_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A & b c= a implies b = a )
assume  b in A ; ::_thesis: ( b c= a implies b = a )
then  b in A \/ B by XBOOLE_0:def_3;
hence  ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum
end;
then  a9 in mi A by A3, Th7;
hence  a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose a in B ; ::_thesis: a in (mi A) \/ B
hence  a in (mi A) \/ B by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  a in (mi A) \/ B ; ::_thesis: verum
end;
hence  mi (A \/ B) c= (mi A) \/ B by Lm2; ::_thesis: verum
end;

theorem Th13: :: SUBSTLAT:13
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) \/ B) = mi (A \/ B)
A1: (mi A) \/ B c= A \/ B by Th8, XBOOLE_1:9;
now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_\/_B)_holds_
a_in_mi_(A_\/_B)
let a be set ; ::_thesis: ( a in mi ((mi A) \/ B) implies a in mi (A \/ B) )
assume A2: a in mi ((mi A) \/ B) ; ::_thesis: a in mi (A \/ B)
then reconsider a9 = a as finite set by Lm1;
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_\/_B_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A \/ B & b c= a implies b = a )
assume that
A4: b in A \/ B and
A5: b c= a ; ::_thesis: b = a
now__::_thesis:_b_=_a
percases ( b in A or b in B ) by A4, XBOOLE_0:def_3;
suppose b in A ; ::_thesis: b = a
then consider c being set  such that
A6: c c= b and
A7: c in mi A by Th10;
 ( c in (mi A) \/ B & c c= a ) by A5, A6, A7, XBOOLE_0:def_3, XBOOLE_1:1;
then  c = a by A2, Th6;
hence  b = a by A5, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose b in B ; ::_thesis: b = a
then  b in (mi A) \/ B by XBOOLE_0:def_3;
hence  b = a by A2, A5, Th6; ::_thesis: verum
end;
end;
end;
hence  b = a ; ::_thesis: verum
end;
 a in (mi A) \/ B by A2, Th6;
then  a9 in mi (A \/ B) by A1, A3, Th7;
hence  a in mi (A \/ B) ; ::_thesis: verum
end;
hence  mi ((mi A) \/ B) c= mi (A \/ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A \/ B) c= mi ((mi A) \/ B)
A8: mi (A \/ B) c= (mi A) \/ B by Th12;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_\/_B)_holds_
a_in_mi_((mi_A)_\/_B)
let a be set ; ::_thesis: ( a in mi (A \/ B) implies a in mi ((mi A) \/ B) )
assume A9: a in mi (A \/ B) ; ::_thesis: a in mi ((mi A) \/ B)
then reconsider a9 = a as finite set by Lm1;
 for b being finite set st b in (mi A) \/ B & b c= a holds
b = a by A1, A9, Th6;
then  a9 in mi ((mi A) \/ B) by A8, A9, Th7;
hence  a in mi ((mi A) \/ B) ; ::_thesis: verum
end;
hence  mi (A \/ B) c= mi ((mi A) \/ B) by Lm2; ::_thesis: verum
end;

theorem Th14: :: SUBSTLAT:14
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
proof
let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies A ^ D c= B ^ D )
deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) ->  set = $1 \/ $2;
defpred S1[ Function, Function] means ( $1 in A & $2 in D & $1 tolerates $2 );
defpred S2[ Function, Function] means ( $1 in B & $2 in D & $1 tolerates $2 );
set X1 =  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t]  }  ;
set X2 =  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  ;
assume  A c= B ; ::_thesis: A ^ D c= B ^ D
then A1: for s, t being Element of PFuncs (V,C) st S1[s,t] holds
S2[s,t] ;
  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S1[s,t]  }  c=  {  H1(s,t) where s, t is Element of PFuncs (V,C) : S2[s,t]  }  from FRAENKEL:sch_2(A1);
hence  A ^ D c= B ^ D ; ::_thesis: verum
end;

theorem Th15: :: SUBSTLAT:15
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let a be set ; ::_thesis: ( a in A ^ B implies ex b, c being set st
( b in A & c in B & a = b \/ c ) )
assume  a in A ^ B ; ::_thesis: ex b, c being set st
( b in A & c in B & a = b \/ c )
then  ex s, t being Element of PFuncs (V,C) st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence  ex b, c being set st
( b in A & c in B & a = b \/ c ) ; ::_thesis: verum
end;

theorem :: SUBSTLAT:16
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;

Lm3:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
let a be finite set ; ::_thesis: ( a in A ^ B implies ex b being finite set st
( b c= a & b in (mi A) ^ B ) )
assume  a in A ^ B ; ::_thesis: ex b being finite set st
( b c= a & b in (mi A) ^ B )
then consider b, c being Element of PFuncs (V,C) such that
A1: a = b \/ c and
A2: b in A and
A3: c in B and
A4: b tolerates c ;
 b is finite by A1, FINSET_1:1, XBOOLE_1:7;
then consider d being set  such that
A5: d c= b and
A6: d in mi A by A2, Th10;
A7: mi A c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider d9 = d, c9 = c as Element of PFuncs (V,C) by A6;
reconsider d1 = d, b1 = b, c1 = c as PartFunc of V,C by A6, A7, PARTFUN1:46;
 d1 c= b1 by A5;
then A8: d9 tolerates c9 by A4, PARTFUN1:58;
then  d9 \/ c9 = d9 +* c9 by FUNCT_4:30;
then reconsider e = d1 \/ c1 as Element of PFuncs (V,C) by PARTFUN1:45;
reconsider e = e as finite set by A1, A5, FINSET_1:1, XBOOLE_1:9;
take  e ; ::_thesis: ( e c= a & e in (mi A) ^ B )
thus  e c= a by A1, A5, XBOOLE_1:9; ::_thesis: e in (mi A) ^ B
thus  e in (mi A) ^ B by A3, A6, A8; ::_thesis: verum
end;

theorem Th17: :: SUBSTLAT:17
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ B) c= (mi A) ^ B
A1: (mi A) ^ B c= A ^ B by Th8, Th14;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_
a_in_(mi_A)_^_B
let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in (mi A) ^ B )
assume A2: a in mi (A ^ B) ; ::_thesis: a in (mi A) ^ B
then  ( a in A ^ B & a is finite ) by Lm1, Th6;
then  ex b being finite set st
( b c= a & b in (mi A) ^ B ) by Lm3;
hence  a in (mi A) ^ B by A1, A2, Th6; ::_thesis: verum
end;
hence  mi (A ^ B) c= (mi A) ^ B by Lm2; ::_thesis: verum
end;

theorem Th18: :: SUBSTLAT:18
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
proof
let V, C be set ; ::_thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
let A, B, D be Element of Fin (PFuncs (V,C)); ::_thesis: ( A c= B implies D ^ A c= D ^ B )
 ( D ^ A = A ^ D & D ^ B = B ^ D ) by Th3;
hence  ( A c= B implies D ^ A c= D ^ B ) by Th14; ::_thesis: verum
end;

theorem Th19: :: SUBSTLAT:19
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((mi A) ^ B) = mi (A ^ B)
A1: (mi A) ^ B c= A ^ B by Th8, Th14;
now__::_thesis:_for_a_being_set_st_a_in_mi_((mi_A)_^_B)_holds_
a_in_mi_(A_^_B)
let a be set ; ::_thesis: ( a in mi ((mi A) ^ B) implies a in mi (A ^ B) )
assume A2: a in mi ((mi A) ^ B) ; ::_thesis: a in mi (A ^ B)
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_A_^_B_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in A ^ B & b c= a implies b = a )
assume  b in A ^ B ; ::_thesis: ( b c= a implies b = a )
then consider c being finite set  such that
A4: c c= b and
A5: c in (mi A) ^ B by Lm3;
assume A6: b c= a ; ::_thesis: b = a
then  c c= a by A4, XBOOLE_1:1;
then  c = a by A2, A5, Th6;
hence  b = a by A4, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
 ( a in (mi A) ^ B & a is finite ) by A2, Lm1, Th6;
hence  a in mi (A ^ B) by A1, A3, Th7; ::_thesis: verum
end;
hence  mi ((mi A) ^ B) c= mi (A ^ B) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi (A ^ B) c= mi ((mi A) ^ B)
A7: mi (A ^ B) c= (mi A) ^ B by Th17;
now__::_thesis:_for_a_being_set_st_a_in_mi_(A_^_B)_holds_
a_in_mi_((mi_A)_^_B)
let a be set ; ::_thesis: ( a in mi (A ^ B) implies a in mi ((mi A) ^ B) )
assume A8: a in mi (A ^ B) ; ::_thesis: a in mi ((mi A) ^ B)
then  ( a is finite & ( for b being finite set st b in (mi A) ^ B & b c= a holds
b = a ) ) by A1, Lm1, Th6;
hence  a in mi ((mi A) ^ B) by A7, A8, Th7; ::_thesis: verum
end;
hence  mi (A ^ B) c= mi ((mi A) ^ B) by Lm2; ::_thesis: verum
end;

theorem Th20: :: SUBSTLAT:20
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ (mi B)) = mi (A ^ B)
 ( A ^ (mi B) = (mi B) ^ A & A ^ B = B ^ A ) by Th3;
hence  mi (A ^ (mi B)) = mi (A ^ B) by Th19; ::_thesis: verum
end;

theorem Th21: :: SUBSTLAT:21
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
proof
let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) = (K ^ L) ^ M
A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th3;
A2: now__::_thesis:_for_K,_L,_M_being_Element_of_Fin_(PFuncs_(V,C))_holds_K_^_(L_^_M)_c=_(K_^_L)_^_M
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L ^ M) c= (K ^ L) ^ M
A3: ( K c= PFuncs (V,C) & L c= PFuncs (V,C) ) by FINSUB_1:def_5;
A4: M c= PFuncs (V,C) by FINSUB_1:def_5;
now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_^_M)_holds_
a_in_(K_^_L)_^_M
let a be set ; ::_thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )
A5: K ^ (L ^ M) c= PFuncs (V,C) by FINSUB_1:def_5;
assume A6: a in K ^ (L ^ M) ; ::_thesis: a in (K ^ L) ^ M
then consider b, c being set  such that
A7: b in K and
A8: c in L ^ M and
A9: a = b \/ c by Th15;
A10: c c= b \/ c by XBOOLE_1:7;
consider b1, c1 being set  such that
A11: b1 in L and
A12: c1 in M and
A13: c = b1 \/ c1 by A8, Th15;
reconsider b2 = b, b12 = b1 as PartFunc of V,C by A3, A7, A11, PARTFUN1:46;
reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3, A4, A7, A11, A12;
 b1 c= c by A13, XBOOLE_1:7;
then A14: ( b c= b \/ c & b1 c= b \/ c ) by A10, XBOOLE_1:1, XBOOLE_1:7;
then A15: b9 tolerates b19 by A6, A9, A5, PARTFUN1:57;
then  b9 \/ b19 = b9 +* b19 by FUNCT_4:30;
then  b2 \/ b12 is PartFunc of V,C ;
then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45;
A16: ( b \/ (b1 \/ c1) = (b \/ b1) \/ c1 & c2 in K ^ L ) by A7, A11, A15, XBOOLE_1:4;
 c1 c= c by A13, XBOOLE_1:7;
then A17: c1 c= b \/ c by A10, XBOOLE_1:1;
 c2 c= b \/ c by A14, XBOOLE_1:8;
then  c2 tolerates c19 by A6, A9, A5, A17, PARTFUN1:57;
hence  a in (K ^ L) ^ M by A9, A12, A13, A16; ::_thesis: verum
end;
hence  K ^ (L ^ M) c= (K ^ L) ^ M by Lm2; ::_thesis: verum
end;
then A18: K ^ (L ^ M) c= (K ^ L) ^ M ;
 ( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th3;
then  (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence  K ^ (L ^ M) = (K ^ L) ^ M by A18, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th22: :: SUBSTLAT:22
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proof
let V, C be set ; ::_thesis: for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
let K, L, M be Element of Fin (PFuncs (V,C)); ::_thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
now__::_thesis:_for_a_being_set_st_a_in_K_^_(L_\/_M)_holds_
a_in_(K_^_L)_\/_(K_^_M)
let a be set ; ::_thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) )
assume A1: a in K ^ (L \/ M) ; ::_thesis: a in (K ^ L) \/ (K ^ M)
then consider b, c being set  such that
A2: b in K and
A3: c in L \/ M and
A4: a = b \/ c by Th15;
 K ^ (L \/ M) c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
 ( K c= PFuncs (V,C) & L \/ M c= PFuncs (V,C) ) by FINSUB_1:def_5;
then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2, A3;
 ( b9 c= a9 & c9 c= a9 ) by A4, XBOOLE_1:7;
then A5: b9 tolerates c9 by PARTFUN1:57;
 ( c9 in L or c9 in M ) by A3, XBOOLE_0:def_3;
then  ( a in K ^ L or a in K ^ M ) by A2, A4, A5;
hence  a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M)
 ( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th18, XBOOLE_1:7;
hence  (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; ::_thesis: verum
end;

Lm4:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
proof
let V, C be set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
let a be set ; ::_thesis: ( a in A ^ B implies ex c being set st
( c in B & c c= a ) )
assume  a in A ^ B ; ::_thesis: ex c being set st
( c in B & c c= a )
then consider b, c being set  such that
 b in A and
A1: c in B and
A2: a = b \/ c by Th15;
take  c ; ::_thesis: ( c in B & c c= a )
thus  c in B by A1; ::_thesis: c c= a
thus  c c= a by A2, XBOOLE_1:7; ::_thesis: verum
end;

Lm5:  for V, C being set
for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
proof
let V, C be set ; ::_thesis: for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
let K, L be Element of Fin (PFuncs (V,C)); ::_thesis: mi ((K ^ L) \/ L) = mi L
now__::_thesis:_for_a_being_set_st_a_in_mi_((K_^_L)_\/_L)_holds_
a_in_mi_L
let a be set ; ::_thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L )
assume A1: a in mi ((K ^ L) \/ L) ; ::_thesis: a in mi L
then  a in (K ^ L) \/ L by Th6;
then A2: ( a in K ^ L or a in L ) by XBOOLE_0:def_3;
A3: now__::_thesis:_for_b_being_finite_set_st_b_in_L_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in L & b c= a implies b = a )
assume  b in L ; ::_thesis: ( b c= a implies b = a )
then  b in (K ^ L) \/ L by XBOOLE_0:def_3;
hence  ( b c= a implies b = a ) by A1, Th6; ::_thesis: verum
end;
A4: now__::_thesis:_(_a_in_K_^_L_implies_a_in_L_)
assume  a in K ^ L ; ::_thesis: a in L
then consider b being set  such that
A5: b in L and
A6: b c= a by Lm4;
 b in (K ^ L) \/ L by A5, XBOOLE_0:def_3;
hence  a in L by A1, A5, A6, Th6; ::_thesis: verum
end;
 a is finite by A1, Lm1;
hence  a in mi L by A2, A4, A3, Th7; ::_thesis: verum
end;
hence  mi ((K ^ L) \/ L) c= mi L by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: mi L c= mi ((K ^ L) \/ L)
now__::_thesis:_for_a_being_set_st_a_in_mi_L_holds_
a_in_mi_((K_^_L)_\/_L)
let a be set ; ::_thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) )
assume A7: a in mi L ; ::_thesis: a in mi ((K ^ L) \/ L)
then A8: a in L by Th6;
then A9: a in (K ^ L) \/ L by XBOOLE_0:def_3;
A10: now__::_thesis:_for_b_being_finite_set_st_b_in_(K_^_L)_\/_L_&_b_c=_a_holds_
b_=_a
let b be finite set ; ::_thesis: ( b in (K ^ L) \/ L & b c= a implies b = a )
assume  b in (K ^ L) \/ L ; ::_thesis: ( b c= a implies b = a )
then A11: ( b in K ^ L or b in L ) by XBOOLE_0:def_3;
assume A12: b c= a ; ::_thesis: b = a
now__::_thesis:_(_b_in_K_^_L_implies_b_in_L_)
assume  b in K ^ L ; ::_thesis: b in L
then consider c being set  such that
A13: c in L and
A14: c c= b by Lm4;
 c c= a by A12, A14, XBOOLE_1:1;
then  c = a by A7, A13, Th6;
hence  b in L by A8, A12, A14, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  b = a by A7, A11, A12, Th6; ::_thesis: verum
end;
 a is finite by A7, Lm1;
hence  a in mi ((K ^ L) \/ L) by A9, A10, Th7; ::_thesis: verum
end;
hence  mi L c= mi ((K ^ L) \/ L) by Lm2; ::_thesis: verum
end;

theorem Th23: :: SUBSTLAT:23
for V, C being set
for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
proof
let V, C be set ; ::_thesis: for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
let B be Element of Fin (PFuncs (V,C)); ::_thesis: B c= B ^ B
now__::_thesis:_for_a_being_set_st_a_in_B_holds_
a_in_B_^_B
let a be set ; ::_thesis: ( a in B implies a in B ^ B )
assume A1: a in B ; ::_thesis: a in B ^ B
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
 ( a = a \/ a & a9 tolerates a9 ) ;
hence  a in B ^ B by A1; ::_thesis: verum
end;
hence  B c= B ^ B by Lm2; ::_thesis: verum
end;

theorem Th24: :: SUBSTLAT:24
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
proof
let V, C be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
let A be Element of Fin (PFuncs (V,C)); ::_thesis: mi (A ^ A) = mi A
thus  mi (A ^ A) = mi ((A ^ A) \/ A) by Th23, XBOOLE_1:12
.= mi A by Lm5 ; ::_thesis: verum
end;

theorem :: SUBSTLAT:25
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
proof
let V, C be set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
let K be Element of SubstitutionSet (V,C); ::_thesis: mi (K ^ K) = K
thus  mi (K ^ K) = mi K by Th24
.= K by Th11 ; ::_thesis: verum
end;

begin

definition
let V, C be set ;
func SubstLatt (V,C) ->  strict LattStr  means :Def4: :: SUBSTLAT:def 4
( the carrier of it = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of it . (A,B) = mi (A \/ B) & the L_meet of it . (A,B) = mi (A ^ B) ) ) );
existence
 ex b1 being strict LattStr st
( the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) )
proof
deffunc H1( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) ->  Element of SubstitutionSet (V,C) = mi ($1 \/ $2);
consider j being BinOp of (SubstitutionSet (V,C)) such that
A1: for x, y being Element of SubstitutionSet (V,C) holds j . (x,y) = H1(x,y) from BINOP_1:sch_4();
deffunc H2( Element of SubstitutionSet (V,C), Element of SubstitutionSet (V,C)) ->  Element of SubstitutionSet (V,C) = mi ($1 ^ $2);
consider m being BinOp of (SubstitutionSet (V,C)) such that
A2: for x, y being Element of SubstitutionSet (V,C) holds m . (x,y) = H2(x,y) from BINOP_1:sch_4();
take  LattStr(# (SubstitutionSet (V,C)),j,m #) ; ::_thesis: ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) )
thus  ( the carrier of LattStr(# (SubstitutionSet (V,C)),j,m #) = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A \/ B) & the L_meet of LattStr(# (SubstitutionSet (V,C)),j,m #) . (A,B) = mi (A ^ B) ) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict LattStr st the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) & the carrier of b2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b2 . (A,B) = mi (A \/ B) & the L_meet of b2 . (A,B) = mi (A ^ B) ) ) holds
b1 = b2
proof
let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) ) & the carrier of A2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ) implies A1 = A2 )
assume that
A3: the carrier of A1 = SubstitutionSet (V,C) and
A4: for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and
A5: the carrier of A2 = SubstitutionSet (V,C) and
A6: for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; ::_thesis: A1 = A2
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (SubstitutionSet (V,C)) by A3, A5;
now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a1_._(x,y)_=_a2_._(x,y)
let x, y be Element of SubstitutionSet (V,C); ::_thesis: a1 . (x,y) = a2 . (x,y)
thus a1 . (x,y) = mi (x \/ y) by A4
.= a2 . (x,y) by A6 ; ::_thesis: verum
end;
then A7: a1 = a2 by BINOP_1:2;
now__::_thesis:_for_x,_y_being_Element_of_SubstitutionSet_(V,C)_holds_a3_._(x,y)_=_a4_._(x,y)
let x, y be Element of SubstitutionSet (V,C); ::_thesis: a3 . (x,y) = a4 . (x,y)
thus a3 . (x,y) = mi (x ^ y) by A4
.= a4 . (x,y) by A6 ; ::_thesis: verum
end;
hence  A1 = A2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def_4_:_
 for V, C being set
for b3 being strict LattStr holds
( b3 = SubstLatt (V,C) iff ( the carrier of b3 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b3 . (A,B) = mi (A \/ B) & the L_meet of b3 . (A,B) = mi (A ^ B) ) ) ) );

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  non empty strict ;
coherence
 not SubstLatt (V,C) is empty
proof
 the carrier of (SubstLatt (V,C)) = SubstitutionSet (V,C) by Def4;
hence  not SubstLatt (V,C) is empty ; ::_thesis: verum
end;
end;

Lm6:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a
set G = SubstLatt (V,C);
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
a "\/" b = mi (b9 \/ a9) by Def4
.= b "\/" a by Def4 ;
hence  a "\/" b = b "\/" a ; ::_thesis: verum
end;

Lm7:  for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
a "\/" (b "\/" c) = the L_join of (SubstLatt (V,C)) . (a,(mi (b9 \/ c9))) by Def4
.= mi ((mi (b9 \/ c9)) \/ a9) by Def4
.= mi (a9 \/ (b9 \/ c9)) by Th13
.= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4
.= mi ((mi (a9 \/ b9)) \/ c9) by Th13
.= the L_join of (SubstLatt (V,C)) . ((mi (a9 \/ b9)),c9) by Def4
.= (a "\/" b) "\/" c by Def4 ;
hence  a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;

   Lm8:  for V, C being set
for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
proof
let V, C be set ; ::_thesis: for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
let K, L be Element of SubstitutionSet (V,C); ::_thesis: the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
thus  the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = the L_join of (SubstLatt (V,C)) . ((mi (K ^ L)),L) by Def4
.= mi ((mi (K ^ L)) \/ L) by Def4
.= mi ((K ^ L) \/ L) by Th13
.= mi L by Lm5
.= L by Th11 ; ::_thesis: verum
end;

Lm9:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
let a, b be Element of (SubstLatt (V,C)); ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
thus (a "/\" b) "\/" b = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,b9)),b9)
.= b by Lm8 ; ::_thesis: verum
end;

Lm10:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
a "/\" b = mi (a9 ^ b9) by Def4
.= mi (b9 ^ a9) by Th3
.= b "/\" a by Def4 ;
hence  a "/\" b = b "/\" a ; ::_thesis: verum
end;

Lm11:  for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let V, C be set ; ::_thesis: for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
let a, b, c be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V,C) by Def4;
set G = SubstLatt (V,C);
a "/\" (b "/\" c) = the L_meet of (SubstLatt (V,C)) . (a,(mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (mi (b9 ^ c9))) by Def4
.= mi (a9 ^ (b9 ^ c9)) by Th20
.= mi ((a9 ^ b9) ^ c9) by Th21
.= mi ((mi (a9 ^ b9)) ^ c9) by Th19
.= the L_meet of (SubstLatt (V,C)) . ((mi (a9 ^ b9)),c9) by Def4
.= (a "/\" b) "/\" c by Def4 ;
hence  a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;

Lm12:  for V, C being set
for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
proof
let V, C be set ; ::_thesis: for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
let K, L, M be Element of SubstitutionSet (V,C); ::_thesis: the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
A1: the L_meet of (SubstLatt (V,C)) . (K,M) = mi (K ^ M) by Def4;
 ( the L_join of (SubstLatt (V,C)) . (L,M) = mi (L \/ M) & the L_meet of (SubstLatt (V,C)) . (K,L) = mi (K ^ L) ) by Def4;
then reconsider La = the L_join of (SubstLatt (V,C)) . (L,M), Lb = the L_meet of (SubstLatt (V,C)) . (K,L), Lc = the L_meet of (SubstLatt (V,C)) . (K,M) as Element of SubstitutionSet (V,C) by A1;
the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = mi (K ^ La) by Def4
.= mi (K ^ (mi (L \/ M))) by Def4
.= mi (K ^ (L \/ M)) by Th20
.= mi ((K ^ L) \/ (K ^ M)) by Th22
.= mi ((mi (K ^ L)) \/ (K ^ M)) by Th13
.= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th13
.= mi (Lb \/ (mi (K ^ M))) by Def4
.= mi (Lb \/ Lc) by Def4 ;
hence  the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M))) by Def4; ::_thesis: verum
end;

Lm13:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a
let a, b be Element of (SubstLatt (V,C)); ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by Def4;
thus a "/\" (a "\/" b) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (a9,a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Lm12
.= the L_join of (SubstLatt (V,C)) . ((mi (a9 ^ a9)),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Def4
.= the L_join of (SubstLatt (V,C)) . ((mi a9),( the L_meet of (SubstLatt (V,C)) . (a9,b9))) by Th24
.= a "\/" (a "/\" b) by Th11
.= (a "/\" b) "\/" a by Lm6
.= (b "/\" a) "\/" a by Lm10
.= a by Lm9 ; ::_thesis: verum
end;

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  strict Lattice-like ;
coherence
 SubstLatt (V,C) is Lattice-like
proof
set G = SubstLatt (V,C);
thus  for u, v being Element of (SubstLatt (V,C)) holds u "\/" v = v "\/" u by Lm6; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( SubstLatt (V,C) is join-associative & SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus  for u, v, w being Element of (SubstLatt (V,C)) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm7; :: according to LATTICES:def_5 ::_thesis: ( SubstLatt (V,C) is meet-absorbing & SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus  for u, v being Element of (SubstLatt (V,C)) holds (u "/\" v) "\/" v = v by Lm9; :: according to LATTICES:def_8 ::_thesis: ( SubstLatt (V,C) is meet-commutative & SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus  for u, v being Element of (SubstLatt (V,C)) holds u "/\" v = v "/\" u by Lm10; :: according to LATTICES:def_6 ::_thesis: ( SubstLatt (V,C) is meet-associative & SubstLatt (V,C) is join-absorbing )
thus  for u, v, w being Element of (SubstLatt (V,C)) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm11; :: according to LATTICES:def_7 ::_thesis: SubstLatt (V,C) is join-absorbing
let u, v be Element of (SubstLatt (V,C)); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u
thus  u "/\" (u "\/" v) = u by Lm13; ::_thesis: verum
end;
end;

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  strict distributive bounded ;
coherence
 ( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )
proof
thus  SubstLatt (V,C) is distributive ::_thesis: SubstLatt (V,C) is bounded
proof
let u, v, w be Element of (SubstLatt (V,C)); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of SubstitutionSet (V,C) by Def4;
thus u "/\" (v "\/" w) = the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M)))
.= (u "/\" v) "\/" (u "/\" w) by Lm12 ; ::_thesis: verum
end;
A1: SubstLatt (V,C) is lower-bounded
proof
reconsider E = {} as Element of SubstitutionSet (V,C) by Th1;
set L = SubstLatt (V,C);
reconsider e = E as Element of (SubstLatt (V,C)) by Def4;
take  e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "/\" b1 = e & b1 "/\" e = e )
let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A2: e "\/" u = mi (E \/ K) by Def4
.= u by Th11 ;
then  u "/\" e = e by LATTICES:def_9;
hence  ( e "/\" u = e & u "/\" e = e ) by A2, LATTICES:def_9; ::_thesis: verum
end;
 SubstLatt (V,C) is upper-bounded
proof
reconsider E = {{}} as Element of SubstitutionSet (V,C) by Th2;
set L = SubstLatt (V,C);
reconsider e = E as Element of (SubstLatt (V,C)) by Def4;
take  e ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (SubstLatt (V,C)) holds
( e "\/" b1 = e & b1 "\/" e = e )
let u be Element of (SubstLatt (V,C)); ::_thesis: ( e "\/" u = e & u "\/" e = e )
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A3: e "/\" u = mi (E ^ K) by Def4
.= mi (K ^ E) by Th3
.= mi K by Th4
.= u by Th11 ;
then  e "\/" u = e by LATTICES:def_8;
hence  ( e "\/" u = e & u "\/" e = e ) by A3, LATTICES:def_8; ::_thesis: verum
end;
hence  SubstLatt (V,C) is bounded by A1; ::_thesis: verum
end;
end;

theorem :: SUBSTLAT:26
for V, C being set holds Bottom (SubstLatt (V,C)) = {}
proof
let V, C be set ; ::_thesis: Bottom (SubstLatt (V,C)) = {}
 {} in SubstitutionSet (V,C) by Th1;
then reconsider Z = {} as Element of (SubstLatt (V,C)) by Def4;
now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"\/"_u_=_u
let u be Element of (SubstLatt (V,C)); ::_thesis: Z "\/" u = u
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "\/" u = mi (z \/ u9) by Def4
.= u by Th11 ; ::_thesis: verum
end;
hence  Bottom (SubstLatt (V,C)) = {} by LATTICE2:14; ::_thesis: verum
end;

theorem :: SUBSTLAT:27
for V, C being set holds Top (SubstLatt (V,C)) = {{}}
proof
let V, C be set ; ::_thesis: Top (SubstLatt (V,C)) = {{}}
 {{}} in SubstitutionSet (V,C) by Th2;
then reconsider Z = {{}} as Element of (SubstLatt (V,C)) by Def4;
now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_Z_"/\"_u_=_u
let u be Element of (SubstLatt (V,C)); ::_thesis: Z "/\" u = u
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "/\" u = mi (z ^ u9) by Def4
.= mi (u9 ^ z) by Th3
.= mi u9 by Th4
.= u by Th11 ; ::_thesis: verum
end;
hence  Top (SubstLatt (V,C)) = {{}} by LATTICE2:16; ::_thesis: verum
end;