HEYTING2

:: Lattice of Substitutions Is a Heyting Algebra
::  by Adam Grabowski
::
:: Received December 31, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, SUBSTLAT, FINSET_1, FUNCT_1, FINSUB_1, PARTFUN1,
      TARSKI, XBOOLE_0, SETWISEO, ORDINAL4, NORMFORM, RELAT_1, ARYTM_1,
      LATTICES, FUNCT_2, HEYTING1, BINOP_1, STRUCT_0, ZFMISC_1, FDIFF_1,
      EQREL_1, LATTICE2, PBOOLE, FUNCOP_1, FILTER_0, XBOOLEAN, HEYTING2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, PARTFUN1, LATTICES,
      STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0;
 constructors FUNCOP_1, SETWISEO, FILTER_0, LATTICE2, HEYTING1, SUBSTLAT,
      RELSET_1, BINOP_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1,
      FINSUB_1, SETWISEO, STRUCT_0, LATTICES, SUBSTLAT, FUNCT_2, RELSET_1,
      PRE_POLY, LATTICE2;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FILTER_0, XBOOLE_0;
 expansions TARSKI, XBOOLE_0;
 theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, PARTFUN1, BINOP_1, LATTICES,
      LATTICE2, RELAT_1, FUNCT_1, FUNCT_2, SUBSTLAT, SETWISEO, FUNCOP_1,
      FILTER_0, HEYTING1, RELSET_1, XBOOLE_0, XBOOLE_1, PRE_POLY;
 schemes FRAENKEL, BINOP_1, LATTICE3, PRE_CIRC, FUNCT_1, FUNCT_2, XBOOLE_0;

begin :: Preliminaries

reserve V, C, x, a, b for set;
reserve A, B for Element of SubstitutionSet (V, C);

theorem Th1:
  for a, b being set st b in SubstitutionSet (V, C) & a in b holds
  a is finite Function
proof
  let a, b be set;
  assume that
A1: b in SubstitutionSet (V, C) and
A2: a in b;
  b in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u
in A holds u is finite ) & for s1, t being Element of PFuncs (V, C) holds ( s1
  in A & t in A & s1 c= t implies s1 = t ) } by A1,SUBSTLAT:def 1;
  then
  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 ) holds ( s in
  A & t in A & s c= t implies s = t );
  hence thesis by A1,A2;
end;

Lm1: for A, B, C be set st A = B \/ C & A c= B holds A = B
by XBOOLE_1:7;

begin :: Some properties of sets of substitutions

theorem Th2:
  for a being finite Element of PFuncs (V, C) holds {a} in
  SubstitutionSet (V, C)
proof
  let a be finite Element of PFuncs (V, C);
A1: for s, t being Element of PFuncs (V,C) holds ( s in { a } & t in { a } &
  s c= t implies s = t )
  proof
    let s, t be Element of PFuncs (V,C);
    assume that
A2: s in { a } and
A3: t in { a } and
    s c= t;
    s = a by A2,TARSKI:def 1;
    hence thesis by A3,TARSKI:def 1;
  end;
  for u being set st u in {a} holds u is finite;
  then
  {.a.} 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) holds (
  s in A & t in A & s c= t implies s = t ) } by A1;
  hence thesis by SUBSTLAT:def 1;
end;

theorem
  A ^ B = A implies for a be set st a in A ex b be set st b in B & b c= a
proof
  assume
A1: A ^ B = A;
  let a be set;
  assume a in A;
  then consider b,c be set such that
  b in A and
A2: c in B and
A3: a = b \/ c by A1,SUBSTLAT:15;
  take c;
  thus thesis by A2,A3,XBOOLE_1:7;
end;

theorem Th4:
  mi (A ^ B) = A implies for a be set st a in A ex b be set st b in B & b c= a
proof
  assume
A1: mi (A ^ B) = A;
  let a be set;
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
  assume a in A;
  then consider b,c be set such that
  b in A and
A3: c in B and
A4: a = b \/ c by A1,A2,SUBSTLAT:15;
  take c;
  thus thesis by A3,A4,XBOOLE_1:7;
end;

theorem Th5:
  (for a be set st a in A ex b be set st b in B & b c= a) implies
  mi (A ^ B) = A
proof
  assume
A1: for a be set st a in A ex b be set st b in B & b c= a;
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
  thus mi (A ^ B) c= A
  proof
    let a be object;
     reconsider aa=a as set by TARSKI:1;
A3: A c= PFuncs (V, C) by FINSUB_1:def 5;
    assume
A4: a in mi (A ^ B);
    then consider b, c be set such that
A5: b in A and
    c in B and
A6: a = b \/ c by A2,SUBSTLAT:15;
A7: b c= aa by A6,XBOOLE_1:7;
    consider b1 be set such that
A8: b1 in B and
A9: b1 c= b by A1,A5;
    B c= PFuncs (V, C) by FINSUB_1:def 5;
    then reconsider b9 = b, b19 = b1 as Element of PFuncs (V, C) by A5,A8,A3;
A10: b = b1 \/ b by A9,XBOOLE_1:12;
    b19 tolerates b9 by A9,PARTFUN1:54;
    then b in A ^ B by A5,A8,A10,SUBSTLAT:16;
    hence thesis by A4,A5,A7,SUBSTLAT:6;
  end;
  thus A c= mi (A ^ B)
  proof
    let a be object;
     reconsider aa=a as set by TARSKI:1;
A11: A c= PFuncs (V, C) by FINSUB_1:def 5;
    assume
A12: a in A;
    then consider b be set such that
A13: b in B and
A14: b c= aa by A1;
    B c= PFuncs (V, C) by FINSUB_1:def 5;
    then reconsider a9 = a, b9 = b as Element of PFuncs (V, C) by A12,A13,A11;
A15: a9 tolerates b9 by A14,PARTFUN1:54;
A16: a in mi A by A12,SUBSTLAT:11;
A17: for b be finite set st b in A ^ B & b c= aa holds b = a
    proof
      let b be finite set;
      assume that
A18:  b in A ^ B and
A19:  b c= aa;
      consider c, d be set such that
A20:  c in A and
      d in B and
A21:  b = c \/ d by A18,SUBSTLAT:15;
      c c= b by A21,XBOOLE_1:7;
      then c c= aa by A19;
      then c = a by A16,A20,SUBSTLAT:6;
      hence thesis by A19,A21,Lm1;
    end;
    a9 = a9 \/ b9 by A14,XBOOLE_1:12;
    then
A22: a9 in A ^ B by A12,A13,A15,SUBSTLAT:16;
    aa is finite by A12,Th1;
    hence thesis by A22,A17,SUBSTLAT:7;
  end;
end;

definition
  let V be set, C be finite set;
  let A be Element of Fin PFuncs (V, C);
  func Involved A -> set means
  :Def1:
   for x being object holds
    x in it iff ex f being finite Function st f in A & x in dom f;
  existence
  proof
    defpred P[object] means
     ex f being finite Function st f in A & $1 in dom f;
    consider X be set such that
A1: for x being object holds x in X iff x in V & P[x] from XBOOLE_0:sch 1;
    take X;
    let x be object;
    thus x in X implies ex f being finite Function st f in A & x in dom f by A1
;
    given f being finite Function such that
A2: f in A and
A3: x in dom f;
    A c= PFuncs (V, C) by FINSUB_1:def 5;
    then
    ex f1 being Function st f = f1 & dom f1 c= V & rng f1 c= C by A2,
PARTFUN1:def 3;
    hence thesis by A1,A2,A3;
  end;
  uniqueness
  proof
    defpred P[object] means
ex f being finite Function st f in A & $1 in dom f;
    let r,s be set such that
A4: for x being object holds
x in r iff ex f being finite Function st f in A & x in dom f and
A5:  for x being object holds
x in s iff ex f being finite Function st f in A & x in dom f;
    for X1,X2 being set st (for x being object holds x in X1 iff P[x]) &
    (for
    x being object holds x in X2 iff P[x]) holds X1 = X2
   from XBOOLE_0:sch 3;
    hence thesis by A4,A5;
  end;
end;

reserve C for finite set;
reserve A, B for Element of SubstitutionSet (V, C);

theorem Th6:
  for V being set, C be finite set, A being Element of Fin PFuncs
  (V, C) holds Involved A c= V
proof
  let V be set, C be finite set, A be Element of Fin PFuncs (V, C);
  let a be object;
  assume a in Involved A;
  then consider f being finite Function such that
A1: f in A and
A2: a in dom f by Def1;
  A c= PFuncs (V, C) by FINSUB_1:def 5;
  then ex f1 being Function st f = f1 & dom f1 c= V & rng f1 c= C by A1,
PARTFUN1:def 3;
  hence thesis by A2;
end;

Lm2: for V being set, C be finite set, A being non empty Element of Fin PFuncs
(V, C) holds Involved A is finite
proof
  deffunc F(Function)=dom $1;
  let V be set, C be finite set, A be non empty Element of Fin PFuncs (V, C);
  defpred P[set] means $1 in A & $1 is finite;
  defpred Q[set] means $1 in A;
  set X = { F(f) where f is Element of PFuncs(V, C) : P[f]};
A1: for x be set st x in X holds x is finite
  proof
    let x be set;
    assume x in X;
    then ex f1 being Element of PFuncs(V, C) st x = dom f1 & f1 in A & f1
    is finite;
    hence thesis;
  end;
A2: A is finite;
A3: { F(f) where f is Element of PFuncs(V, C) : f in A } is finite from
  FRAENKEL:sch 21(A2);
  for x be object holds x in Involved A iff ex Y be set st x in Y & Y in X
  proof
    let x be object;
    hereby
      assume x in Involved A;
      then consider f being finite Function such that
A4:   f in A and
A5:   x in dom f by Def1;
      A c= PFuncs (V,C) by FINSUB_1:def 5;
      then dom f in X by A4;
      hence ex Y be set st x in Y & Y in X by A5;
    end;
    given Y be set such that
A6: x in Y and
A7: Y in X;
    ex f1 being Element of PFuncs(V, C) st Y = dom f1 & f1 in A & f1
    is finite by A7;
    hence thesis by A6,Def1;
  end;
  then
A8: Involved A = union X by TARSKI:def 4;
A9: for g being Element of PFuncs(V, C) holds P[g] implies Q[g];
  X c= { F(f) where f is Element of PFuncs(V, C) : Q[f]} from FRAENKEL:sch
  1(A9);
  hence thesis by A3,A8,A1,FINSET_1:7;
end;

theorem Th7:
  for V being set, C being finite set, A being Element of Fin
  PFuncs (V, C) st A = {} holds Involved A = {}
proof
  let V be set, C be finite set, A be Element of Fin PFuncs (V, C);
  assume
A1: A = {};
  assume Involved A <> {};
  then consider x be object such that
A2: x in Involved A by XBOOLE_0:def 1;
  ex f being finite Function st f in A & x in dom f by A2,Def1;
  hence thesis by A1;
end;

registration
  let V be set, C being finite set, A being Element of Fin PFuncs (V, C);
  cluster Involved A -> finite;
coherence
proof
  per cases;
  suppose
    A is non empty;
    hence thesis by Lm2;
  end;
  suppose
    A is empty;
    hence thesis by Th7;
  end;
end;
end;

theorem
  for C being finite set, A being Element of Fin PFuncs ({}, C) holds
  Involved A = {} by Th6,XBOOLE_1:3;

definition
  let V be set, C be finite set;
  let A be Element of Fin PFuncs (V, C);
  func -A -> Element of Fin PFuncs (V, C) equals
  { f where f is Element of
PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not
  f tolerates g };
  coherence
  proof
    deffunc F(set)=$1;
    defpred Q[set] means not contradiction;
    defpred P[Element of PFuncs (Involved A, C)] means for h be Element of
    PFuncs (V, C) st h in A holds not $1 tolerates h;
    set M = { f where f is Element of PFuncs (Involved A, C) : for g be
    Element of PFuncs (V, C) st g in A holds not f tolerates g };
A1: the set of all  f where f is Element of PFuncs (Involved A, C)
    c= PFuncs (Involved A, C)
    proof
      let a be object;
      assume a in the set of all
 f where f is Element of PFuncs (Involved A, C) ;
      then ex f1 be Element of PFuncs (Involved A, C) st f1 = a & not
      contradiction;
      hence thesis;
    end;
A2: for v being Element of PFuncs (Involved A, C) holds P[v] implies Q[v];
A3: { F(f) where f is Element of PFuncs (Involved A, C) : P[f] } c= { F(f)
where f is Element of PFuncs (Involved A, C) : Q[f] } from FRAENKEL:sch 1(A2);
A4: M c= PFuncs (V, C)
    proof
      let a be object;
      assume a in M;
      then ex f1 be Element of PFuncs (Involved A, C) st f1 = a & for g be
      Element of PFuncs (V, C) st g in A holds not f1 tolerates g;
      then
A5:   a in PFuncs (Involved A, C);
      Involved A c= V by Th6;
      then PFuncs (Involved A, C) c= PFuncs (V, C) by PARTFUN1:50;
      hence thesis by A5;
    end;
    PFuncs (Involved A, C) is finite by PRE_POLY:17;
    hence thesis by A3,A1,A4,FINSUB_1:def 5;
  end;
end;

theorem Th9:
  A ^ -A = {}
proof
  assume A ^ -A <> {};
  then consider x be object such that
A1: x in A ^ -A by XBOOLE_0:def 1;
  x in { s \/ t where s, t is Element of PFuncs (V,C) : s in A & t in -A &
  s tolerates t } by A1,SUBSTLAT:def 3;
  then consider s1, t1 be Element of PFuncs (V,C) such that
  x = s1 \/ t1 and
A2: s1 in A and
A3: t1 in -A and
A4: s1 tolerates t1;
  ex f1 be Element of PFuncs (Involved A, C) st f1 = t1 & for g be
  Element of PFuncs (V, C) st g in A holds not f1 tolerates g by A3;
  hence thesis by A2,A4;
end;

theorem Th10:
  A = {} implies -A = { {} }
proof
  defpred P[Element of PFuncs (Involved A, C)] means for g be Element of
  PFuncs (V, C) st g in A holds not $1 tolerates g;
  assume
A1: A = {};
  then
A2: for g be Element of PFuncs (V, C) st g in A holds not {} tolerates g;
  { xx where xx is Element of PFuncs (Involved A, C) : P[xx]} c= PFuncs (
  Involved A, C) from FRAENKEL:sch 10;
  then -A c= PFuncs ({}, C) by A1,Th7;
  then
A3: -A c= { {} } by PARTFUN1:48;
  {} in { {} } by TARSKI:def 1;
  then {} in PFuncs ({}, C) by PARTFUN1:48;
  then {} in PFuncs (Involved A, C) by A1,Th7;
  then {} in -A by A2;
  then { {} } c= -A by ZFMISC_1:31;
  hence thesis by A3;
end;

theorem
  A = { {} } implies -A = {}
proof
  assume
A1: A = {{}};
  assume -A <> {};
  then consider x1 be object such that
A2: x1 in -A by XBOOLE_0:def 1;
  consider f1 being Element of PFuncs (Involved A, C) such that
  x1 = f1 and
A3: for g be Element of PFuncs (V, C) st g in {{}} holds not f1
  tolerates g by A1,A2;
A4: {} in {{}} by TARSKI:def 1;
  {} is PartFunc of V, C by RELSET_1:12;
  then
A5: {} in PFuncs (V, C) by PARTFUN1:45;
  f1 tolerates {} by PARTFUN1:59;
  hence thesis by A3,A5,A4;
end;

theorem Th12:
  for V being set, C being finite set for A being Element of
  SubstitutionSet (V, C) holds mi (A ^ -A) = Bottom SubstLatt (V,C)
proof
  let V be set, C be finite set, A be Element of SubstitutionSet (V, C);
  mi (A ^ -A) = {} by Th9,SUBSTLAT:9
    .= Bottom SubstLatt (V,C) by SUBSTLAT:26;
  hence thesis;
end;

theorem
  for V being non empty set, C being finite non empty set for A being
  Element of SubstitutionSet (V, C) st A = {} holds mi -A = Top SubstLatt (V,C)
proof
  let V be non empty set, C be finite non empty set, A be Element of
  SubstitutionSet (V, C);
  assume A = {};
  then
A1: -A = { {} } by Th10;
  then -A in SubstitutionSet (V, C) by SUBSTLAT:2;
  then mi -A = { {} } by A1,SUBSTLAT:11;
  hence thesis by SUBSTLAT:27;
end;

theorem Th14:
  for V being set, C being finite set for A being Element of
  SubstitutionSet (V, C), a being Element of PFuncs (V, C), B being Element of
SubstitutionSet (V, C) st B = { a } holds A ^ B = {} implies ex b being finite
  set st b in -A & b c= a
proof
  let V, C;
  let A be Element of SubstitutionSet (V, C);
  let a be Element of PFuncs (V, C);
  let B be Element of SubstitutionSet (V, C) such that
A1: B = { a };
  assume
A2: A ^ B = {};
  per cases;
  suppose
A3: A is non empty;
    then reconsider AA = A as finite non empty set;
    defpred P[Element of PFuncs (V, C),set] means $2 in dom $1 /\ dom a & $1.
    $2 <> a.$2;
    defpred P[set] means not contradiction;
A4: ex kk be Function st kk = a & dom kk c= V & rng kk c= C by PARTFUN1:def 3;
A5: now
      let s be Element of PFuncs (V, C) such that
A6:   s in A;
      not s tolerates a
      proof
        assume
A7:     s tolerates a;
        a in B by A1,TARSKI:def 1;
        then s \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) : s1
        in A & t1 in B & s1 tolerates t1 } by A6,A7;
        hence thesis by A2,SUBSTLAT:def 3;
      end;
      then consider x be object such that
A8:   x in dom s /\ dom a and
A9:   s.x <> a.x by PARTFUN1:def 4;
      consider a9 be Function such that
A10:  a9 = a and
A11:  dom a9 c= V and
      rng a9 c= C by PARTFUN1:def 3;
      dom s /\ dom a c= dom a9 by A10,XBOOLE_1:17;
      then dom s /\ dom a c= V by A11;
      then reconsider x as Element of [V] by A8,HEYTING1:def 2;
      take x;
      thus P[s,x] by A8,A9;
    end;
    consider g be Element of Funcs (PFuncs (V, C), [V]) such that
A12: for s be Element of PFuncs (V, C) st s in A holds P[s,g.s] from
    FRAENKEL:sch 27(A5);
    deffunc G(set)=g.$1;
A13: A = [A] by A3,HEYTING1:def 2;
    { G(b) where b is Element of AA : P[b] } is finite from PRE_CIRC:sch
    1;
    then reconsider
    UKA = the set of all  g.b where b is Element of [A]  as
    finite set by A13;
    set f = a|UKA;
A14: dom f c= Involved A
    proof
      let x be object;
      assume x in dom f;
      then x in UKA by RELAT_1:57;
      then consider b be Element of [A] such that
A15:  x = g.b;
      reconsider b as finite Function by A13,Th1;
      reconsider b9 = b as Element of PFuncs (V, C) by A13,SETWISEO:9;
      g.b9 in dom b9 /\ dom a by A13,A12;
      then x in dom b by A15,XBOOLE_0:def 4;
      hence thesis by A13,Def1;
    end;
    rng f c= rng a by RELAT_1:70;
    then rng f c= C by A4;
    then reconsider f9 = f as Element of PFuncs (Involved A, C) by A14,
PARTFUN1:def 3;
    for g be Element of PFuncs (V, C) st g in A holds not f tolerates g
    proof
      let g1 be Element of PFuncs (V, C);
      reconsider g9 = g1 as Function;
      assume
A16:  g1 in A;
      ex z be set st z in dom g1 /\ dom f & g9.z <> f.z
      proof
        set z = g.g1;
        take z;
A17:    z in dom g1 /\ dom a by A12,A16;
        then
A18:    z in dom a by XBOOLE_0:def 4;
        z in the set of all  g.b1 where b1 is Element of [A]  by A13,A16;
        then z in dom a /\ UKA by A18,XBOOLE_0:def 4;
        then
A19:    z in dom f by RELAT_1:61;
        z in dom g1 by A17,XBOOLE_0:def 4;
        hence z in dom g1 /\ dom f by A19,XBOOLE_0:def 4;
        g1.z <> a.z by A12,A16;
        hence thesis by A19,FUNCT_1:47;
      end;
      hence thesis by PARTFUN1:def 4;
    end;
    then f9 in { f1 where f1 is Element of PFuncs (Involved A, C) : for g be
    Element of PFuncs (V, C) st g in A holds not f1 tolerates g };
    hence thesis by RELAT_1:59;
  end;
  suppose
A20: A is empty;
    reconsider K = {} as finite set;
    take K;
    -A = {{}} by A20,Th10;
    hence thesis by TARSKI:def 1;
  end;
end;

definition
  let V be set, C be finite set;
  let A, B be Element of Fin PFuncs (V, C);
  func A =>> B -> Element of Fin PFuncs (V, C) equals
  PFuncs (V, C) /\ { union
  {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of
  PFuncs (A, B) : dom f = A };
  coherence
  proof
    reconsider PF = PFuncs (A, B) as functional finite non empty set
           by PRE_POLY:17;
    set Z = { union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
    where f is Element of PFuncs (A, B) : dom f = A};
    set K = PFuncs (V, C) /\ Z;
A1: Z c= { union {f.i \ i where i is Element of PFuncs (V, C) : i in A }
    where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A }
    proof
      let z be object;
      assume z in Z;
      then
      ex f1 be Element of PFuncs (A, B) st z = union {f1.i \ i where i is
      Element of PFuncs (V, C) : i in A} & dom f1 = A;
      hence thesis;
    end;
    defpred P[Element of PF] means $1 in PFuncs(A,B) & dom $1 = A;
    deffunc F(Element of PF)= union {$1.i \ i where i is Element of PFuncs (V,
    C) : i in A};
A2: { F(f) where f is Element of PF : P[f]} is finite from PRE_CIRC:sch 1;
    K c= PFuncs (V, C) by XBOOLE_1:17;
    hence thesis by A1,A2,FINSUB_1:def 5;
  end;
end;

theorem Th15:
  for A, B being Element of Fin PFuncs (V, C), s being set st s in
  A =>> B holds ex f being PartFunc of A, B st s = union {f.i \ i where i is
  Element of PFuncs (V, C) : i in A} & dom f = A
proof
  let A, B be Element of Fin PFuncs (V, C), s be set;
  assume s in A =>> B;
  then s in { union {f.i \ i where i is Element of PFuncs (V, C) : i in A}
  where f is Element of PFuncs (A, B) : dom f = A} by XBOOLE_0:def 4;
  then consider f be Element of PFuncs (A, B) such that
A1: s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A} and
A2: dom f = A;
  f is PartFunc of A, B by PARTFUN1:47;
  hence thesis by A1,A2;
end;

Lm3: for V be set, C be finite set, A be Element of Fin PFuncs (V, C), K be
Element of SubstitutionSet (V, C) holds a in A ^ (A =>> K) implies ex b st b in
K & b c= a
proof
  let V be set, C be finite set, A be Element of Fin PFuncs (V, C), K be
  Element of SubstitutionSet (V, C);
A1: K c= PFuncs (V, C) by FINSUB_1:def 5;
  assume a in A ^ (A =>> K);
  then consider b,c be set such that
A2: b in A and
A3: c in A =>> K and
A4: a = b \/ c by SUBSTLAT:15;
  A c= PFuncs (V, C) by FINSUB_1:def 5;
  then reconsider b9 = b as Element of PFuncs (V, C) by A2;
  consider f be PartFunc of A, K such that
A5: c = union {f.i \ i where i is Element of PFuncs (V, C) : i in A } and
A6: dom f = A by A3,Th15;
  f.b in K by A2,A6,PARTFUN1:4;
  then reconsider d = f.b as Element of PFuncs (V, C) by A1;
  take d;
  thus d in K by A2,A6,PARTFUN1:4;
  d \ b9 in {f.i \ i where i is Element of PFuncs (V, C) : i in A} by A2;
  hence thesis by A4,A5,XBOOLE_1:44,ZFMISC_1:74;
end;

theorem
  for V being set, C being finite set, A being Element of Fin PFuncs (V,
  C ) st A = {} holds A =>> A = {{}}
proof
  deffunc G(set)={};
  let V be set, C be finite set, A be Element of Fin PFuncs (V, C);
  defpred P[Function] means dom $1 = A;
  deffunc F(Element of PFuncs (A, A))= union {$1.i \ i where i is Element of
  PFuncs (V, C) : i in A};
A1: ex a being Element of PFuncs (A, A) st P[a]
  proof
    reconsider e = id A as Element of PFuncs (A, A) by PARTFUN1:45;
    take e;
    thus thesis;
  end;
A2: { {} where f is Element of PFuncs (A, A) : P[f] } = {{}} from LATTICE3:
  sch 1 (A1);
  assume
A3: A = {};
  now
    let f be Element of PFuncs (A, A);
    not ex x be object st x in {f.i \ i where i is Element of PFuncs (V, C) :
    i in A}
    proof
      given x be object such that
A4:   x in {f.i \ i where i is Element of PFuncs (V, C) : i in A};
      ex x1 being Element of PFuncs (V, C) st x = f.x1 \ x1 & x1 in A by A4;
      hence contradiction by A3;
    end;
    hence {f.i \ i where i is Element of PFuncs (V, C) : i in A} = {} by
XBOOLE_0:def 1;
  end;
  then
A5: for v being Element of PFuncs (A, A) st P[v] holds F(v) = G(v) by
ZFMISC_1:2;
A6: { F(f) where f is Element of PFuncs (A, A) : P[f]} = { G(f) where f is
  Element of PFuncs (A, A) : P[f] } from FRAENKEL:sch 6 (A5);
  {} 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;
  hence thesis by A6,A2,XBOOLE_1:28;
end;

reserve u, v for Element of SubstLatt (V, C);
reserve s, t, a, b for Element of PFuncs (V,C);
reserve K, L for Element of SubstitutionSet (V, C);

Lm4: for X being set st X c= K holds X in SubstitutionSet (V, C)
proof
  let X be set;
  assume
A1: X c= K;
  K c= PFuncs (V, C) by FINSUB_1:def 5;
  then X c= PFuncs (V, C) by A1;
  then reconsider B = X as Element of Fin PFuncs (V, C) by A1,FINSUB_1:def 5;
A2: for a,b st a in B & b in B & a c= b holds a = b by A1,SUBSTLAT:5;
  for x be set st x in X holds x is finite by A1,Th1;
  then
  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) holds ( s in
  A & t in A & s c= t implies s = t ) } by A2;
  hence thesis by SUBSTLAT:def 1;
end;

theorem Th17:
  for X being set st X c= u holds X is Element of SubstLatt (V, C)
proof
  let X be set;
  reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
  assume X c= u;
  then X c= u9;
  then X in SubstitutionSet (V, C) by Lm4;
  hence thesis by SUBSTLAT:def 4;
end;

begin :: Lattice of substitutions is implicative

definition
  let V, C;
  func pseudo_compl (V, C) -> UnOp of the carrier of SubstLatt (V, C) means
  :
  Def4: for
 u9 being Element of SubstitutionSet (V, C) st u9 = u holds it.u = mi(
  -u9);
  existence
  proof
    deffunc F(Element of SubstitutionSet (V, C))=mi(-$1);
    consider IT being Function of SubstitutionSet (V, C), SubstitutionSet (V,
    C) such that
A1: for u being Element of SubstitutionSet (V, C) holds IT.u = F(u)
    from FUNCT_2:sch 4;
    SubstitutionSet (V, C) = the carrier of SubstLatt (V, C) by SUBSTLAT:def 4;
    then reconsider IT as UnOp of the carrier of SubstLatt (V, C);
    take IT;
    thus thesis by A1;
  end;
  correctness
  proof
    let IT,IT9 be UnOp of the carrier of SubstLatt (V, C);
    assume that
A2: for u9 being Element of SubstitutionSet (V, C) st u9 = u holds IT.
    u = mi (-u9) and
A3: for u9 being Element of SubstitutionSet (V, C) st u9 = u holds IT9
    .u = mi (-u9);
    now
      let u;
      reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
      thus IT.u = mi (-u9) by A2
        .= IT9.u by A3;
    end;
    hence IT = IT9 by FUNCT_2:63;
  end;
  func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means
  :
  Def5: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9 = v
  holds it.(u,v) = mi (u9 =>> v9);
  existence
  proof
    set ZA = the carrier of SubstLatt (V, C);
    defpred P[set, set, set] means for u9, v9 being Element of SubstitutionSet
    (V, C) st u9 = $1 & v9 = $2 holds $3 = mi (u9 =>> v9);
A4: for x,y being Element of ZA ex z being Element of ZA st P[x,y,z]
    proof
      let x,y be Element of ZA;
      reconsider x9 = x, y9 = y as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
      reconsider z = mi (x9 =>> y9) as Element of ZA by SUBSTLAT:def 4;
      take z;
      let u9, v9 be Element of SubstitutionSet (V, C);
      assume that
A5:   u9 = x and
A6:   v9 = y;
      thus thesis by A5,A6;
    end;
    consider o being BinOp of the carrier of SubstLatt (V, C) such that
A7: for a,b being Element of SubstLatt (V, C) holds P[a,b,o.(a,b)]
    from BINOP_1:sch 3(A4);
    take o;
    let u,v;
    let u9, v9 be Element of SubstitutionSet (V, C);
    assume that
A8: u9 = u and
A9: v9 = v;
    thus thesis by A7,A8,A9;
  end;
  correctness
  proof
    let IT1,IT2 be BinOp of the carrier of SubstLatt (V, C);
    assume that
A10: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9
    = v holds IT1.(u,v) = mi (u9 =>> v9) and
A11: for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9
    = v holds IT2.(u,v) = mi (u9 =>> v9);
    now
      let u, v;
      reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
      thus IT1.(u,v) = mi (u9 =>> v9) by A10
        .= IT2.(u,v) by A11;
    end;
    hence IT1 = IT2 by BINOP_1:2;
  end;
  let u;
  func SUB u -> Element of Fin the carrier of SubstLatt (V, C) equals
  bool u;
  coherence
  proof
    reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
A12: bool u c= the carrier of SubstLatt (V, C)
    proof
      let x be object;
      assume x in bool u;
      then x is Element of SubstLatt (V, C) by Th17;
      hence thesis;
    end;
    u9 is finite;
    hence thesis by A12,FINSUB_1:def 5;
  end;
  correctness;
  func diff(u) -> UnOp of the carrier of SubstLatt (V, C) means
  :Def7:
  it.v = u \ v;
  existence
  proof
    deffunc F(set)=u \ $1;
    consider IT being Function such that
A13: dom IT = the carrier of SubstLatt (V, C) & for v be set st v in
    the carrier of SubstLatt (V, C) holds IT.v = F(v) from FUNCT_1:sch 5;
    u in the carrier of SubstLatt (V, C);
    then
A14: u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
    for x be object st x in the carrier of SubstLatt (V, C) holds IT.x in
    Fin PFuncs (V, C)
    proof
      let x be object;
      assume
A15:     x in the carrier of SubstLatt (V, C);
      reconsider x as set by TARSKI:1;
A16:  IT.x = u \ x by A13,A15;
      u \ x in SubstitutionSet (V,C) by A14,Lm4;
      hence thesis by A16;
    end;
    then reconsider
    IT as Function of the carrier of SubstLatt (V, C), Fin PFuncs (
    V, C) by A13,FUNCT_2:3;
    now
      let v be Element of SubstLatt (V, C);
      u \ v in SubstitutionSet (V,C) by A14,Lm4;
      then IT.v in SubstitutionSet (V,C) by A13;
      hence IT.v in the carrier of SubstLatt (V, C) by SUBSTLAT:def 4;
    end;
    then reconsider IT as UnOp of the carrier of SubstLatt (V, C) by HEYTING1:1
;
    take IT;
    let v;
    thus thesis by A13;
  end;
  correctness
  proof
    let IT,IT9 be UnOp of the carrier of SubstLatt (V, C);
    assume that
A17: IT.v = u \ v and
A18: IT9.v = u \ v;
    now
      let v be Element of SubstLatt (V, C);
      thus IT.v = u \ v by A17
        .= IT9.v by A18;
    end;
    hence IT = IT9 by FUNCT_2:63;
  end;
end;

Lm5: v in SUB u implies v "\/" (diff u).v = u
proof
  assume
A1: v in SUB u;
  reconsider u9 = u, v9 = v, dv = (diff u).v as Element of SubstitutionSet (V,
  C) by SUBSTLAT:def 4;
A2: u \ v = (diff u).v by Def7;
  thus v "\/" (diff u).v = (the L_join of SubstLatt (V,C)).(v, (diff u).v) by
LATTICES:def 1
    .= mi ( v9 \/ dv ) by SUBSTLAT:def 4
    .= mi u9 by A1,A2,XBOOLE_1:45
    .= u by SUBSTLAT:11;
end;

Lm6: for K be Element of Fin PFuncs (V, C) st K = {a} holds ex v be Element of
SubstitutionSet (V,C) st v in SUB u & v ^ K = {} & for b st b in (diff u).v
holds b tolerates a
proof
  deffunc F(set)=$1;
  let K be Element of Fin PFuncs (V, C) such that
A1: K = {a};
  deffunc F1(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
  defpred Q[Element of PFuncs (V, C)] means not $1 tolerates a & $1 in u & $1
  tolerates a;
  deffunc F(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2;
  defpred P[Element of PFuncs (V, C)] means $1 is finite & not $1 tolerates a;
  set M = { F(s) where s is Element of PFuncs (V, C): F(s) in u & P[s] };
  defpred P[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $1 in M &
  $2 in { a } & $1 tolerates $2;
  defpred Q[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $2 = a &
  $1 in M & $1 tolerates $2;
  defpred P[Element of PFuncs (V, C)] means $1 in M & $1 tolerates a;
  defpred P1[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $1 in M
  & $1 tolerates $2;
  deffunc F(Element of PFuncs (V, C))=$1 \/ a;
A2: M c= u from FRAENKEL:sch 17;
  then reconsider v = M as Element of SubstLatt (V, C) by Th17;
  reconsider v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
  take v;
  thus v in SUB u by A2;
A3: P[s,t] iff Q[s,t] by TARSKI:def 1;
A4: { F(s,t): P[s,t] } = { F(s9,t9) where s9, t9 is Element of PFuncs (V, C)
  : Q[s9,t9] } from FRAENKEL:sch 4(A3);
  s in M iff s is finite & not s tolerates a & s in u
  proof
    thus s in M implies s is finite & not s tolerates a & s in u
    proof
      assume s in M;
      then ex s2 be Element of PFuncs (V, C) st s2 = s & s2 in u & s2 is
      finite & not s2 tolerates a;
      hence thesis;
    end;
    thus thesis;
  end;
  then
A5: P[s] iff Q[s];
A6: { F(s9) where s9 is Element of PFuncs (V, C) : P[s9]} = { F(s): Q[s]}
  from FRAENKEL:sch 3(A5);
  { F1(s,t) where t is Element of PFuncs (V, C) : t = a & P1[s,t]} = { F1(
  s9,a) where s9 is Element of PFuncs (V, C) : P1[s9,a]} from FRAENKEL:sch 20;
  then
A7: v ^ K = { s \/ a: not s tolerates a & s in u & s tolerates a } by A1,A4,A6,
SUBSTLAT:def 3;
  thus v ^ K = {}
  proof
    assume v ^ K <> {};
    then consider x be object such that
A8: x in v ^ K by XBOOLE_0:def 1;
    ex s1 be Element of PFuncs (V, C) st x = s1 \/ a &( not s1 tolerates
    a)& s1 in u & s1 tolerates a by A7,A8;
    hence thesis;
  end;
  let b;
  assume b in (diff u).v;
  then
A9: b in u \ v by Def7;
  then
A10: not b in M by XBOOLE_0:def 5;
  u in the carrier of SubstLatt (V, C);
  then u in SubstitutionSet (V, C) by SUBSTLAT:def 4;
  then b is finite by A9,Th1;
  hence thesis by A9,A10;
end;

definition
  let V, C;
  func Atom(V, C) -> Function of PFuncs (V, C), the carrier of SubstLatt (V, C
  ) means
  :Def8:
  for a being Element of PFuncs (V,C) holds it.a = mi {.a.};
  existence
  proof
    deffunc F(Element of PFuncs (V, C))= mi {.$1.};
    consider f be Function of PFuncs (V, C), SubstitutionSet (V, C) such that
A1: for a be Element of PFuncs (V, C) holds f.a = F(a) from FUNCT_2:
    sch 4;
A2: the carrier of SubstLatt (V, C) = SubstitutionSet (V, C) by SUBSTLAT:def 4;
A3: now
      let x be object;
      assume x in PFuncs (V, C);
      then reconsider a = x as Element of PFuncs (V, C);
      f.a = mi {.a.} by A1;
      hence f.x in the carrier of SubstLatt (V, C) by A2;
    end;
    dom f = PFuncs (V, C) by FUNCT_2:def 1;
    then reconsider
    f as Function of PFuncs (V, C), the carrier of SubstLatt (V, C
    ) by A3,FUNCT_2:3;
    take f;
    thus thesis by A1;
  end;
  correctness
  proof
    let IT1,IT2 be Function of PFuncs (V, C), the carrier of SubstLatt (V, C)
    such that
A4: for a holds IT1.a = mi {.a.} and
A5: for a holds IT2.a = mi {.a.};
    now
      let a;
      IT1.a = mi {.a.} by A4;
      hence IT1.a = IT2.a by A5;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

Lm7: for a be Element of PFuncs (V, C) st a is finite holds Atom (V, C).a = {a
}
proof
  let a be Element of PFuncs (V, C);
A1: for s, t being Element of PFuncs (V,C) holds ( s in { a } & t in { a } &
  s c= t implies s = t )
  proof
    let s, t be Element of PFuncs (V,C);
    assume that
A2: s in { a } and
A3: t in { a } and
    s c= t;
    s = a by A2,TARSKI:def 1;
    hence thesis by A3,TARSKI:def 1;
  end;
  assume a is finite;
  then for u being set st u in { a } holds u is finite;
  then
  {.a.} 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) holds (
  s in A & t in A & s c= t implies s = t ) } by A1;
  then { a } in SubstitutionSet (V, C) by SUBSTLAT:def 1;
  then {a} = mi {.a.} by SUBSTLAT:11
    .= Atom (V, C).a by Def8;
  hence thesis;
end;

theorem Th18:
  FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C))
proof
  deffunc F(Element of Fin PFuncs (V, C))= mi $1;
A1: FinUnion(K,singleton PFuncs (V, C)) c= mi (FinUnion(K,singleton PFuncs
  (V, C)))
  proof
    let a be object;
     reconsider aa=a as set by TARSKI:1;
    assume
A2: a in FinUnion(K,singleton PFuncs (V, C));
    then consider b be Element of PFuncs (V, C) such that
A3: b in K and
A4: a in (singleton PFuncs (V, C)).b by SETWISEO:57;
A5: a = b by A4,SETWISEO:55;
A6: now
      K in SubstitutionSet (V, C);
      then
      K 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) holds (
      s in A & t in A & s c= t implies s = t ) } by SUBSTLAT:def 1;
      then
A7:   ex AA be Element of Fin PFuncs (V,C) st K = AA & ( for u being set
st u in AA holds u is finite ) & for s, t being Element of PFuncs (V, C) holds
      ( s in AA & t in AA & s c= t implies s = t );
      let s be finite set;
      assume that
A8:  s in FinUnion(K,singleton PFuncs (V, C)) and
A9:  s c= aa;
      consider t such that
A10:  t in K and
A11:  s in (singleton PFuncs (V, C)).t by A8,SETWISEO:57;
      s = t by A11,SETWISEO:55;
      hence s = a by A3,A5,A9,A10,A7;
    end;
    aa is finite by A3,A5,Th1;
    hence thesis by A2,A6,SUBSTLAT:7;
  end;
  consider g being Function of Fin PFuncs (V, C), SubstitutionSet (V,C) such
  that
A12: for B be Element of Fin PFuncs (V, C) holds g.B = F(B) from FUNCT_2:
  sch 4;
  reconsider g as Function of Fin PFuncs (V, C), the carrier of SubstLatt (V,
  C) by SUBSTLAT:def 4;
A13: now
    let x,y be Element of Fin PFuncs (V, C);
A14: g.x = mi x by A12;
A15: g.y = mi y by A12;
    thus g.(x \/ y) = mi (x \/ y) by A12
      .= mi (mi x \/ y) by SUBSTLAT:13
      .= mi (mi x \/ mi y) by SUBSTLAT:13
      .= (the L_join of SubstLatt (V, C)).(g.x,g.y) by A14,A15,SUBSTLAT:def 4;
  end;
A16: now
    let a be object;
    assume
A17: a in K;
    then reconsider a9 = a as Element of PFuncs (V, C) by SETWISEO:9;
A18: a9 is finite by A17,Th1;
    then reconsider KL = {a9} as Element of SubstitutionSet (V,C) by Th2;
    thus ((g*singleton PFuncs (V, C))|K).a = (g*singleton PFuncs (V, C)).a by
A17,FUNCT_1:49
      .= g.(singleton PFuncs (V, C) .a9) by FUNCT_2:15
      .= g.{a} by SETWISEO:54
      .= mi KL by A12
      .= KL by SUBSTLAT:11
      .= Atom (V, C).a9 by A18,Lm7
      .= (Atom (V, C)|K).a by A17,FUNCT_1:49;
  end;
A19: mi (FinUnion(K,singleton PFuncs (V, C))) c= FinUnion(K,singleton PFuncs
  (V, C)) by SUBSTLAT:8;
A20: rng singleton PFuncs (V, C) c= Fin PFuncs (V, C);
A21: K c= PFuncs (V, C) by FINSUB_1:def 5;
  then K c= dom (Atom(V, C)) by FUNCT_2:def 1;
  then
A22: dom (Atom(V, C)|K) = K by RELAT_1:62;
  reconsider gs = g*singleton PFuncs (V, C) as Function of PFuncs (V, C), the
  carrier of SubstLatt (V, C);
A23: g.{}.PFuncs (V, C) = mi {}.PFuncs (V, C) by A12
    .= {} by SUBSTLAT:9
    .= Bottom SubstLatt (V, C) by SUBSTLAT:26
    .= the_unity_wrt the L_join of SubstLatt (V, C) by LATTICE2:18;
  dom g = Fin PFuncs (V, C) by FUNCT_2:def 1;
  then
A24: dom ((g*singleton PFuncs (V, C))) = dom singleton PFuncs (V, C) by A20,
RELAT_1:27;
  dom singleton PFuncs (V, C) = PFuncs (V, C) by FUNCT_2:def 1;
  then dom ((g*singleton PFuncs (V, C))|K) = K by A21,A24,RELAT_1:62;
  hence FinJoin(K, Atom (V, C)) = FinJoin(K, gs) by A22,A16,FUNCT_1:2
,LATTICE2:53
    .= (the L_join of SubstLatt (V, C)) $$(K,gs) by LATTICE2:def 3
    .= g.(FinUnion(K,singleton PFuncs (V, C))) by A23,A13,SETWISEO:53
    .= mi (FinUnion(K,singleton PFuncs (V, C))) by A12
    .= FinUnion(K,singleton PFuncs (V, C)) by A19,A1;
end;

theorem Th19:
  for u being Element of SubstitutionSet (V, C) holds u = FinJoin(
  u, Atom (V, C))
proof
  let u be Element of SubstitutionSet (V, C);
  thus u = FinUnion(u, singleton PFuncs (V, C)) by SETWISEO:58
    .= FinJoin(u, Atom(V, C)) by Th18;
end;

Lm8: (for a be set st a in u ex b be set st b in v & b c= a) implies u [= v
proof
  assume
A1: for a be set st a in u ex b be set st b in v & b c= a;
  reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
  u "/\" v = (the L_meet of SubstLatt (V, C)).(u9, v9) by LATTICES:def 2
    .= mi (u9 ^ v9) by SUBSTLAT:def 4
    .= u9 by A1,Th5;
  hence thesis by LATTICES:4;
end;

theorem Th20:
  (diff u).v [= u
proof
  (diff u).v = u \ v by Def7;
  then for a be set st a in (diff u).v ex b be set st b in u & b c= a;
  hence thesis by Lm8;
end;

theorem Th21:
  for a being Element of PFuncs (V, C) st a is finite for c being
  set st c in Atom(V, C).a holds c = a
proof
  let a be Element of PFuncs (V, C);
  assume a is finite;
  then Atom(V, C).a = { a } by Lm7;
  hence thesis by TARSKI:def 1;
end;

theorem Th22:
  for a being Element of PFuncs (V, C) st K = {a} & L = u & L ^ K
  = {} holds Atom(V, C).a [= pseudo_compl(V, C).u
proof
  let a be Element of PFuncs (V, C);
  assume that
A1: K = {a} and
A2: L = u and
A3: L ^ K = {};
  a in K by A1,TARSKI:def 1;
  then
A4: a is finite by Th1;
  now
    let c be set;
    assume
A5: c in Atom(V, C).a;
    then reconsider c9 = c as Element of PFuncs (V, C) by A4,Th21;
    c = a by A4,A5,Th21;
    then consider b be finite set such that
A6: b in -L and
A7: b c= c9 by A1,A3,Th14;
    consider d be set such that
A8: d c= b and
A9: d in mi(-L) by A6,SUBSTLAT:10;
    take e = d;
    thus e in pseudo_compl(V, C).u by A2,A9,Def4;
    thus e c= c by A7,A8;
  end;
  hence thesis by Lm8;
end;

theorem Th23:
  for a being finite Element of PFuncs (V,C) holds a in Atom(V, C) .a
proof
  let a be finite Element of PFuncs (V,C);
  Atom(V, C).a = { a } by Lm7;
  hence thesis by TARSKI:def 1;
end;

Lm9: u [= v implies for x be set st x in u ex b be set st b in v & b c= x
proof
  reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
  assume u [= v;
  then u = u "/\" v by LATTICES:4
    .= (the L_meet of SubstLatt (V, C)).(u,v) by LATTICES:def 2
    .= mi (u9 ^ v9) by SUBSTLAT:def 4;
  hence thesis by Th4;
end;

theorem Th24:
  for u, v being Element of SubstitutionSet (V, C) holds ((for c
being set st c in u ex b being set st b in v & b c= c \/ a) implies ex b being
  set st b in u =>> v & b c= a )
proof
  let u, v be Element of SubstitutionSet (V, C);
  reconsider u9 = u as Element of SubstLatt (V, C) by SUBSTLAT:def 4;
  defpred P[set,set] means $2 in v & $2 c= $1 \/ a;
  assume that
A1: for b be set st b in u ex c be set st c in v & c c= b \/ a;
A2: now
    let b be Element of PFuncs (V, C);
    assume b in u;
    then consider c be set such that
A3: c in v and
A4: c c= b \/ a by A1;
    v c= PFuncs (V, C) by FINSUB_1:def 5;
    then reconsider c as Element of PFuncs (V, C) by A3;
    take x = c;
    thus P[b,x] by A3,A4;
  end;
  consider f9 be Element of Funcs(PFuncs (V, C), PFuncs (V, C)) such that
A5: b in u implies P[b,f9.b] from FRAENKEL:sch 27(A2);
  set g = f9|u;
  consider f2 be Function such that
A6: f9 = f2 and
  dom f2 = PFuncs (V, C) and
  rng f2 c= PFuncs (V, C) by FUNCT_2:def 2;
  u c= PFuncs (V, C) by FINSUB_1:def 5;
  then g is Function of u, PFuncs (V, C) by FUNCT_2:32;
  then
A7: dom g = u by FUNCT_2:def 1;
  for b be object st b in u holds g.b in v
  proof
    let b be object;
    assume
A8: b in u;
    u c= PFuncs (V, C) by FINSUB_1:def 5;
    then reconsider b9 = b as Element of PFuncs (V, C) by A8;
    g.b9 = f2.b9 by A6,A8,FUNCT_1:49;
    hence thesis by A5,A6,A8;
  end;
  then g is Function of u, v by A7,FUNCT_2:3;
  then
A9: rng g c= v by RELAT_1:def 19;
A10: for b be set st b in u9 holds g.b c= b \/ a
  proof
    let b be set;
    assume
A11: b in u9;
    u c= PFuncs (V, C) by FINSUB_1:def 5;
    then reconsider b9 = b as Element of PFuncs (V, C) by A11;
    g.b9 = f2.b9 by A6,A11,FUNCT_1:49;
    hence thesis by A5,A6,A11;
  end;
  reconsider g as Element of PFuncs (u, v) by A7,A9,PARTFUN1:def 3;
  set d = union {g.i \ i where i is Element of PFuncs (V, C) : i in u9};
A12: d c= a
  proof
    let x be object;
    assume x in d;
    then consider Y be set such that
A13: x in Y and
A14: Y in {g.i \ i where i is Element of PFuncs (V, C) : i in u9} by
TARSKI:def 4;
    consider j be Element of PFuncs (V, C) such that
A15: Y = g.j \ j and
A16: j in u9 by A14;
    g.j c= j \/ a by A10,A16;
    then g.j \j c= a by XBOOLE_1:43;
    hence thesis by A13,A15;
  end;
  then reconsider d as Element of PFuncs (V, C) by PRE_POLY:15;
  take d;
  d in { union {f.i \ i where i is Element of PFuncs (V, C) : i in u}
  where f is Element of PFuncs (u, v) : dom f = u } by A7;
  hence d in u =>> v by XBOOLE_0:def 4;
  thus thesis by A12;
end;

theorem Th25:
  for a being finite Element of PFuncs (V,C) st (for b being
Element of PFuncs (V, C) st b in u holds b tolerates a ) & u "/\" Atom(V, C).a
  [= v holds Atom(V, C).a [= StrongImpl(V, C).(u, v)
proof
  let a be finite Element of PFuncs (V,C);
  assume that
A1: for b be Element of PFuncs (V, C) st b in u holds b tolerates a and
A2: u "/\" Atom(V, C).a [= v;
  reconsider u9 = u, v9 = v, Aa = (Atom(V, C).a) as Element of SubstitutionSet
  (V, C) by SUBSTLAT:def 4;
A3: now
    let c be set;
A4: a in Aa by Th23;
    assume
A5: c in u;
    then
A6: c in u9;
    then reconsider c9 = c as Element of PFuncs (V, C) by SETWISEO:9;
    c9 tolerates a by A1,A5;
    then
    c \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) : s1 in u9
    & t1 in Aa & s1 tolerates t1 } by A5,A4;
    then
A7: c \/ a in u9 ^ Aa by SUBSTLAT:def 3;
    c is finite by A6,Th1;
    then consider b be set such that
A8: b c= c \/ a and
A9: b in mi(u9 ^ Aa) by A7,SUBSTLAT:10;
    b in (the L_meet of SubstLatt (V, C)).(u, Atom(V, C).a) by A9,
SUBSTLAT:def 4;
    then b in u "/\" (Atom (V, C).a) by LATTICES:def 2;
    then consider d be set such that
A10: d in v and
A11: d c= b by A2,Lm9;
    take e = d;
    thus e in v by A10;
    thus e c= c \/ a by A8,A11;
  end;
  now
    let c be set;
    assume
A12: c in Atom(V, C).a;
    then c = a by Th21;
    then consider b be set such that
A13: b in u9 =>> v9 and
A14: b c= c by A3,Th24;
    c in Aa by A12;
    then c is finite by Th1;
    then consider d be set such that
A15: d c= b and
A16: d in mi(u9 =>> v9) by A13,A14,SUBSTLAT:10;
    take e = d;
    thus e in (StrongImpl(V, C).(u, v)) by A16,Def5;
    thus e c= c by A14,A15;
  end;
  hence thesis by Lm8;
end;

deffunc M(set, set) = the L_meet of SubstLatt ($1, $2);

theorem Th26:
  u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C)
proof
  reconsider u9 = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
  thus u "/\" pseudo_compl(V, C).u = M(V, C).(u, pseudo_compl(V, C).u) by
LATTICES:def 2
    .= M(V, C).(u, mi(-u9)) by Def4
    .= mi(u9 ^ mi(-u9)) by SUBSTLAT:def 4
    .= mi(u9 ^ -u9) by SUBSTLAT:20
    .= Bottom SubstLatt (V, C) by Th12;
end;

theorem Th27:
  u "/\" StrongImpl(V, C).(u, v) [= v
proof
  now
    reconsider u9 = u, v9 = v as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
    let a be set;
    assume
A1: a in u "/\" StrongImpl(V, C).(u, v);
    u "/\" StrongImpl(V, C).(u, v) = M(V, C).(u, StrongImpl(V, C).(u, v))
    by LATTICES:def 2
      .= M(V, C).(u, mi(u9 =>> v9)) by Def5
      .= mi(u9 ^ mi(u9 =>> v9)) by SUBSTLAT:def 4
      .= mi(u9 ^ (u9 =>> v9)) by SUBSTLAT:20;
    then a in u9 ^ (u9 =>> v9) by A1,SUBSTLAT:6;
    hence ex b be set st b in v & b c= a by Lm3;
  end;
  hence thesis by Lm8;
end;

Lm10: now
  let V, C, u, v;
  deffunc IMPL(Element of SubstLatt (V, C), Element of SubstLatt (V, C)) =
FinJoin(SUB $1, M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff $1, $2))
  );
  set Psi = M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v));
  reconsider v9 = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4;
A1: now
    let w be Element of SubstLatt (V, C);
    set u2 = (diff u).w, pc = pseudo_compl(V, C).w, si = StrongImpl(V, C).(u2,
    v);
A2: w "/\" (pc "/\" si) = (w "/\" pc) "/\" si by LATTICES:def 7
      .= Bottom SubstLatt (V, C) "/\" si by Th26
      .= Bottom SubstLatt (V, C);
    assume w in SUB u;
    then
A3: w "\/" u2 = u by Lm5;
    M(V, C)[;](u, Psi).w = M(V, C).(u, Psi.w) by FUNCOP_1:53
      .= u "/\" Psi.w by LATTICES:def 2
      .= u "/\" M(V, C).(pc, StrongImpl(V, C)[:](diff u, v).w) by FUNCOP_1:37
      .= u "/\" (pc "/\" StrongImpl(V, C)[:](diff u, v).w) by LATTICES:def 2
      .= u "/\" (pc "/\" si) by FUNCOP_1:48
      .= (w "/\" (pc "/\" si)) "\/" (u2 "/\" (pc "/\" si)) by A3,
LATTICES:def 11
      .= u2 "/\" (si "/\" pc) by A2
      .= (u2 "/\" si) "/\" pc by LATTICES:def 7;
    then
A4: M(V, C)[;](u, Psi).w [= u2 "/\" si by LATTICES:6;
    u2 "/\" si [= v by Th27;
    hence M(V, C)[;](u, Psi).w [= v by A4,LATTICES:7;
  end;
  u "/\" IMPL(u,v) = FinJoin(SUB u, M(V, C)[;](u, Psi)) by LATTICE2:66;
  hence u "/\" IMPL(u,v) [= v by A1,LATTICE2:54;
  let w be Element of SubstLatt (V, C);
  assume
A5: u "/\" v [= w;
A6: v = FinJoin(v9, Atom(V, C)) by Th19;
  then
A7: u "/\" v = FinJoin(v9, M(V, C)[;](u, Atom(V, C))) by LATTICE2:66;
  now
    set pf = pseudo_compl(V, C), sf = StrongImpl(V, C)[:](diff u, w);
    let a be Element of PFuncs (V, C);
    reconsider SA = {.a.} as Element of Fin PFuncs (V, C);
    consider v be Element of SubstitutionSet (V, C) such that
A8: v in SUB u and
A9: v ^ SA = {} and
A10: for b be Element of PFuncs (V, C) st b in (diff u).v holds b
    tolerates a by Lm6;
    assume
A11: a in v9;
    then
A12: a is finite by Th1;
    reconsider v9 = v as Element of SubstLatt (V, C) by SUBSTLAT:def 4;
    set dv = (diff u).v9;
    M(V, C)[;](u, Atom(V, C)).a [= w by A7,A5,A11,LATTICE2:31;
    then M(V, C).(u, Atom(V, C).a) [= w by FUNCOP_1:53;
    then
A13: u "/\" Atom(V, C).a [= w by LATTICES:def 2;
    a is finite by A11,Th1;
    then reconsider SS = {a} as Element of SubstitutionSet (V, C) by Th2;
    v ^ SS = {} by A9;
    then
A14: Atom(V, C).a [= pf.v9 by Th22;
    dv "/\" Atom(V, C).a [= u "/\" Atom(V, C).a by Th20,LATTICES:9;
    then dv "/\" Atom(V, C).a [= w by A13,LATTICES:7;
    then Atom(V, C).a [= StrongImpl(V, C).((diff u).v9, w) by A10,A12,Th25;
    then
A15: Atom(V, C).a [= sf.v9 by FUNCOP_1:48;
    pf.v9"/\" sf.v9 = M(V, C).(pf.v9, sf.v9) by LATTICES:def 2
      .= M(V, C).:(pf, sf).v9 by FUNCOP_1:37;
    then Atom(V, C).a [= M(V, C).:(pf, sf).v9 by A14,A15,FILTER_0:7;
    hence Atom(V, C).a [= IMPL(u,w) by A8,LATTICE2:29;
  end;
  hence v [= IMPL(u,w) by A6,LATTICE2:54;
end;

Lm11: SubstLatt (V, C) is implicative
proof
  let p,q be Element of SubstLatt (V, C);
  take r = FinJoin(SUB p,M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](
  diff p, q)));
  thus p "/\" r [= q & for r1 being Element of SubstLatt (V, C) st p "/\" r1
  [= q holds r1 [= r by Lm10;
end;

registration
  let V, C;
  cluster SubstLatt (V, C) -> implicative;
  coherence by Lm11;
end;

theorem
  u => v = FinJoin(SUB u, (the L_meet of SubstLatt (V, C)).:(
  pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v)))
proof
  deffunc IMPL(Element of SubstLatt (V, C), Element of SubstLatt (V, C)) =
FinJoin(SUB $1,M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff $1, $2)))
  ;
A1: for w be Element of SubstLatt (V, C) st u "/\" w [= v holds w [= IMPL(u,
  v) by Lm10;
  u "/\" IMPL(u,v) [= v by Lm10;
  hence thesis by A1,FILTER_0:def 7;
end;