OPENLATT

:: Representation Theorem for Heyting Lattices
::  by Jolanta Kamie\'nska
::
:: Received July 14, 1993
:: Copyright (c) 1993-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 LATTICE2, FILTER_0, LATTICES, PRE_TOPC, SUBSET_1, XBOOLE_0,
      TOPS_1, TARSKI, RCOMP_1, SETFAM_1, BINOP_1, FUNCT_1, EQREL_1, STRUCT_0,
      PBOOLE, CARD_FIL, INT_2, RELAT_1, ZFMISC_1, ORDINAL1, GROUP_6, FUNCT_2,
      WELLORD1, XBOOLEAN, LATTICE4, OPENLATT;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICES,
      LATTICE2, FILTER_0, LATTICE4;
 constructors BINOP_1, DOMAIN_1, TOPS_1, LATTICE2, FILTER_1, LATTICE4,
      RELSET_1, FILTER_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC,
      FILTER_0, LATTICE2, TOPS_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, PRE_TOPC, FILTER_0, LATTICE4, FUNCT_1, STRUCT_0, XBOOLE_0;
 equalities FILTER_0, LATTICES, STRUCT_0, SUBSET_1;
 expansions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, XBOOLE_0,
      FUNCT_2;
 theorems PRE_TOPC, LATTICES, TOPS_1, ZFMISC_1, FILTER_0, SETFAM_1, TARSKI,
      FUNCT_1, FUNCT_2, LATTICE4, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1,
      STRUCT_0, EQREL_1;
 schemes BINOP_1, DOMAIN_1, FUNCT_1, BINOP_2;

begin

registration
  cluster Heyting -> implicative for 0_Lattice;
  coherence;
  cluster implicative -> upper-bounded for Lattice;
  coherence;
end;

reserve T for TopSpace;
reserve A,B for Subset of T;

theorem Th1:
  A /\ Int(A` \/ B) c= B
proof
A1: A misses A` by XBOOLE_1:79;
  A /\ (A` \/ B) = (A /\ A`) \/ A /\ B by XBOOLE_1:23
    .= {} \/ A /\ B by A1
    .= A /\ B;
  then
A2: A /\ (A` \/ B)c= B by XBOOLE_1:17;
  A /\ Int(A` \/ B) c= A /\ (A` \/ B) by TOPS_1:16,XBOOLE_1:26;
  hence thesis by A2;
end;

theorem Th2:
  for C being Subset of T st C is open & A /\ C c= B holds C c= Int (A` \/ B)
proof
  let C be Subset of T;
  assume that
A1: C is open and
A2: A /\ C c= B;
A3: C c= C \/ A` by XBOOLE_1:7;
  (A /\ C) \/ A` = (A \/ A`) /\ (C \/ A`) by XBOOLE_1:24
    .= [#] T /\ (C \/ A`) by PRE_TOPC:2
    .= C \/ A` by XBOOLE_1:28;
  then C \/ A` c= B \/ A` by A2,XBOOLE_1:9;
  then C c= B \/ A` by A3;
  then Int(C) c= Int(A` \/ B) by TOPS_1:19;
  hence thesis by A1,TOPS_1:23;
end;

definition
  let T be TopStruct;
  func Topology_of T -> Subset-Family of T equals
  the topology of T;
  coherence;
end;

registration
  let T;
  cluster Topology_of T -> non empty;
  coherence;
end;

definition
  let T be non empty TopSpace, P, Q be Element of Topology_of T;
  redefine func P \/ Q -> Element of Topology_of T;  :: redefines \/ (XBOOLE_0, definition)
  coherence
  proof
    reconsider A = P, B = Q as Subset of T;
A1: B is open;
    A is open;
    then P \/ Q is open by A1;
    hence thesis;
  end;
  redefine func P /\ Q -> Element of Topology_of T;  :: redefines /\ (XBOOLE_0, definition)
  coherence
  proof
    reconsider A = P, B = Q as Subset of T;
A2: B is open;
    A is open;
    then P /\ Q is open by A2;
    hence thesis;
  end;
end;

reserve T for non empty TopSpace;
reserve P,Q for Element of Topology_of T;

definition
  let T;
  func Top_Union T -> BinOp of Topology_of T means
  :Def2:
  it.(P,Q) = P \/ Q;
  existence
  proof
    deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 \/ $2;
    thus ex F being BinOp of Topology_of T st for P,Q being Element of
    Topology_of T holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
  end;
  uniqueness
  proof
    set A = Topology_of T;
    deffunc O(Element of A, Element of A) = $1 \/ $2;
    thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
    o2 from BINOP_2:sch 2;
  end;
  func Top_Meet T -> BinOp of Topology_of T means
  :Def3:
  it.(P,Q) = P /\ Q;
  existence
  proof
    deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 /\ $2;
    thus ex F being BinOp of Topology_of T st for P,Q being Element of
    Topology_of T holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
  end;
  uniqueness
  proof
    set A = Topology_of T;
    deffunc O(Element of A, Element of A) = $1 /\ $2;
    thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
    o2 from BINOP_2:sch 2;
  end;
end;

theorem Th3:
  for T being non empty TopSpace holds LattStr(#Topology_of T,
    Top_Union T,Top_Meet T#) is Lattice
proof
  let T;
  set L = LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
A1: now
    let p,q be Element of L;
    thus p "\/" q = q \/ p by Def2
      .= q"\/"p by Def2;
  end;
A2: now
    let p,q be Element of L;
    thus (p"/\"q)"\/"q = p"/\"q \/ q by Def2
      .= (p /\ q) \/ q by Def3
      .= q by XBOOLE_1:22;
  end;
A3: now
    let p,q be Element of L;
    thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Def3
      .= p /\ (p \/ q) by Def2
      .= p by XBOOLE_1:21;
  end;
A4: now
    let p,q,r be Element of L;
    thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Def3
      .= p /\ (q /\ r) by Def3
      .= (p /\ q) /\ r by XBOOLE_1:16
      .= p "/\" q /\ r by Def3
      .= (p"/\"q)"/\"r by Def3;
  end;
A5: now
    let p,q be Element of L;
    thus p "/\" q =q /\ p by Def3
      .= q"/\"p by Def3;
  end;
  now
    let p,q,r be Element of L;
    thus p"\/"(q"\/"r) = p \/ q "\/" r by Def2
      .= p \/ (q \/ r) by Def2
      .= (p \/ q) \/ r by XBOOLE_1:4
      .= p "\/" q \/ r by Def2
      .= (p"\/"q)"\/"r by Def2;
  end;
  then L is join-commutative join-associative meet-absorbing meet-commutative
  meet-associative join-absorbing by A1,A2,A5,A4,A3;
  hence thesis;
end;

definition
  let T;
  func Open_setLatt(T) -> Lattice equals
  LattStr(#Topology_of T,Top_Union T,
    Top_Meet T#);
  coherence by Th3;
end;

theorem
  the carrier of Open_setLatt(T) = Topology_of T;

reserve p,q for Element of Open_setLatt(T);

theorem
  p "\/" q = p \/ q & p "/\" q = p /\ q by Def2,Def3;

theorem Th6:
  p [= q iff p c= q
proof
  p "\/" q = p \/ q by Def2;
  hence thesis by XBOOLE_1:7,12;
end;

theorem Th7:
  for p9,q9 being Element of Topology_of T st p=p9 & q=q9 holds p
  [= q iff p9 c= q9
proof
  let p9,q9 be Element of Topology_of T such that
A1: p=p9 and
A2: q=q9;
  hereby
    assume
A3: p [= q;
    p9 \/ q9 = p"\/"q by A1,A2,Def2
      .= q9 by A2,A3;
    hence p9 c= q9 by XBOOLE_1:7;
  end;
  assume
A4: p9 c= q9;
  p "\/" q = p9 \/ q9 by A1,A2,Def2
    .=q by A2,A4,XBOOLE_1:12;
  hence thesis;
end;

registration
  let T;
  cluster Open_setLatt(T) -> implicative;
coherence
proof
  set OL=Open_setLatt(T);
  let p,q be Element of OL;
  reconsider p9=p, q9=q as Element of Topology_of T;
  reconsider r9= Int(p9` \/ q9) as Element of Topology_of T by PRE_TOPC:def 2;
  reconsider r=r9 as Element of OL;
  take r;
A1: p "/\" r = p9 /\ r9 by Def3;
  p9 /\ r c= q9 by Th1;
  hence p "/\" r [= q by A1,Th7;
  let r1 be Element of OL;
  reconsider r2 = r1 as Element of Topology_of T;
  reconsider r19= r2 as Subset of T;
A2: r19 is open;
  assume
A3: p "/\" r1 [= q;
  p "/\" r1 = p9 /\ r19 by Def3;
  then p9 /\ r2 c= q9 by A3,Th7;
  then r19 c= r9 by A2,Th2;
  hence r1 [= r by Th7;
end;
end;

theorem Th8:
  Open_setLatt(T) is lower-bounded & Bottom Open_setLatt(T) = {}
proof
  set OL=Open_setLatt(T);
  reconsider r = {} as Element of OL by PRE_TOPC:1;
A1: now
    let p;
    thus r"/\"p = r /\ p by Def3
      .= r;
    hence p"/\"r=r;
  end;
  thus OL is lower-bounded
  by A1;
  hence thesis by A1,LATTICES:def 16;
end;

registration
  let T;
  cluster Open_setLatt(T) -> Heyting;
  coherence
  proof
    reconsider OL=Open_setLatt(T) as 0_Lattice by Th8;
    OL is I_Lattice;
    hence thesis;
  end;
end;

theorem Th9:
  Top Open_setLatt(T) = the carrier of T
proof
  set OL=Open_setLatt(T);
  reconsider B = the carrier of T as Element of OL by PRE_TOPC:def 1;
  now
    let p be Element of OL;
    reconsider p9=p as Element of Topology_of T;
    thus B"\/"p = (the carrier of T) \/ p9 by Def2
      .= B by XBOOLE_1:12;
    hence p"\/"B = B;
  end;
  hence thesis by LATTICES:def 17;
end;

reserve L for D_Lattice;
reserve F for Filter of L;
reserve a,b for Element of L;
reserve x,X,X1,X2,Y,Z for set;

definition
  let L;
  func F_primeSet(L) -> set equals
  { F: F <> the carrier of L & F is prime};
  coherence;
end;

theorem Th10:
  F in F_primeSet(L) iff F <> the carrier of L & F is prime
proof
  F in F_primeSet(L) iff ex F0 being Filter of L st F0=F & F0 <> the
  carrier of L & F0 is prime;
  hence thesis;
end;

definition
  let L;
  func StoneH(L) -> Function means
  :Def6:
  dom it = the carrier of L & it.a = { F: F in F_primeSet(L) & a in F};
  existence
  proof
    deffunc F(object) = { F :F in F_primeSet(L) & $1 in F};
    consider f being Function such that
A1: dom f = the carrier of L &
for x being object st x in the carrier of L holds f.
    x = F(x) from FUNCT_1:sch 3;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f1,f2 be Function;
    assume that
A2: dom f1 = the carrier of L & f1.a={ F :F in F_primeSet(L) & a in F} and
A3: dom f2 = the carrier of L & f2.a={ F :F in F_primeSet(L) & a in F};
    now
      let x be object;
      assume x in the carrier of L;
      then reconsider a=x as Element of L;
      thus f1.x = { F :F in F_primeSet(L) & a in F} by A2
        .= f2.x by A3;
    end;
    hence thesis by A2,A3;
  end;
end;

theorem Th11:
  F in StoneH(L).a iff F in F_primeSet(L) & a in F
proof
  StoneH(L).a = {F0 where F0 is Filter of L: F0 in F_primeSet(L) & a in F0
  } by Def6;
  then
  F in StoneH(L).a iff ex F0 being Filter of L st F=F0 & F0 in F_primeSet(
  L) & a in F0;
  hence thesis;
end;

theorem Th12:
  x in StoneH(L).a iff ex F st F=x & F <> the carrier of L & F is
  prime & a in F
proof
A1: StoneH(L).a = {F: F in F_primeSet(L) & a in F} by Def6;
  hereby
    assume x in StoneH(L).a;
    then consider F such that
A2: x=F and
A3: F in F_primeSet(L) and
A4: a in F by A1;
A5: F is prime by A3,Th10;
    F <> the carrier of L by A3,Th10;
    hence ex F st F=x & F <> the carrier of L & F is prime & a in F by A2,A4,A5
;
  end;
  given F such that
A6: F=x and
A7: F <> the carrier of L and
A8: F is prime and
A9: a in F;
  F in F_primeSet(L) by A7,A8;
  hence thesis by A1,A6,A9;
end;

definition
  let L;
  func StoneS(L) -> set equals
  rng StoneH(L);
  coherence;
end;

registration
  let L;
  cluster StoneS(L) -> non empty;
  coherence
  proof
    dom StoneH(L) = the carrier of L by Def6;
    hence thesis by RELAT_1:42;
  end;
end;

theorem Th13:
  x in StoneS(L) iff ex a st x=StoneH(L).a
proof
  hereby
    assume x in StoneS(L);
    then consider y be object such that
A1: y in dom StoneH(L) and
A2: x = StoneH(L).y by FUNCT_1:def 3;
    reconsider y as Element of L by A1,Def6;
    take y;
    thus x=StoneH(L).y by A2;
  end;
  given b such that
A3: x=StoneH(L).b;
  b in the carrier of L;
  then b in dom StoneH(L) by Def6;
  hence thesis by A3,FUNCT_1:def 3;
end;

theorem Th14:
  StoneH(L).(a "\/" b) = StoneH(L).a \/ StoneH(L).b
proof
  set c = a "\/" b;
  hereby
    set c = a "\/" b;
    let x be object;
    assume x in StoneH(L).c;
    then consider F such that
A1: x=F and
A2: F <> the carrier of L and
A3: F is prime and
A4: c in F by Th12;
    a in F or b in F by A3,A4;
    then F in StoneH(L).a or F in StoneH(L).b by A2,A3,Th12;
    hence x in StoneH(L).a \/ StoneH(L).b by A1,XBOOLE_0:def 3;
  end;
  let x be object;
  assume x in StoneH(L).a \/ StoneH(L).b;
  then x in StoneH(L).a or x in StoneH(L).b by XBOOLE_0:def 3;
  then
  (ex F st x=F & F <> the carrier of L & F is prime & a in F ) or ex F st
  x=F & F <> the carrier of L & F is prime & b in F by Th12;
  then consider F such that
A5: x=F and
A6: F <> the carrier of L and
A7: F is prime and
A8: a in F or b in F;
  c in F by A7,A8;
  hence thesis by A5,A6,A7,Th12;
end;

theorem Th15:
  StoneH(L).(a "/\" b) = StoneH(L).a /\ StoneH(L).b
proof
  set c = a "/\" b;
  hereby
    set c = a "/\" b;
    let x be object;
    assume x in StoneH(L).c;
    then consider F such that
A1: x=F and
A2: F <> the carrier of L and
A3: F is prime and
A4: c in F by Th12;
    b in F by A4,FILTER_0:8;
    then
A5: F in StoneH(L).b by A2,A3,Th12;
    a in F by A4,FILTER_0:8;
    then F in StoneH(L).a by A2,A3,Th12;
    hence x in StoneH(L).a /\ StoneH(L).b by A1,A5,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A6: x in StoneH(L).a /\ StoneH(L).b;
  then x in StoneH(L).b by XBOOLE_0:def 4;
  then
A7: ex F st x=F & F <> the carrier of L & F is prime & b in F by Th12;
  x in StoneH(L).a by A6,XBOOLE_0:def 4;
  then ex F st x=F & F <> the carrier of L & F is prime & a in F by Th12;
  then consider F such that
A8: x=F and
A9: F <> the carrier of L and
A10: F is prime and
A11: a in F and
A12: b in F by A7;
  c in F by A11,A12,FILTER_0:8;
  hence thesis by A8,A9,A10,Th12;
end;

definition
  let L, a;
  func SF_have a -> Subset-Family of L equals
  { F : a in F };
  coherence
  proof
    set A= { F : a in F};
    A c= bool the carrier of L
    proof
      let x be object;
      assume x in A;
      then ex F st x=F & a in F;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let L;
  let a;
  cluster SF_have a -> non empty;
  coherence
  proof
    a in <.a.);
    then <.a.) in { F : a in F};
    hence thesis;
  end;
end;

theorem Th16:
  x in SF_have a iff x is Filter of L & a in x
proof
  x in SF_have a iff ex F st F=x & a in F;
  hence thesis;
end;

Lm1: F in SF_have b \ SF_have a iff b in F & not a in F
proof
  F in SF_have b \ SF_have a iff F in SF_have b & not F in SF_have a by
XBOOLE_0:def 5;
  hence thesis by Th16;
end;

theorem Th17:
  x in SF_have b \ SF_have a implies x is Filter of L & b in x & not a in x
proof
  assume
A1: x in SF_have b \ SF_have a;
  then
A2: not x in SF_have a by XBOOLE_0:def 5;
A3: x in SF_have b by A1,XBOOLE_0:def 5;
  then x is Filter of L by Th16;
  hence thesis by A3,A2,Th16;
end;

theorem Th18:
  for Z st Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear
  ex Y st Y in SF_have b \ SF_have a & for X1 st X1 in Z holds X1 c= Y
proof
  let Z;
  assume that
A1: Z <> {} and
A2: Z c= SF_have b \ SF_have a and
A3: Z is c=-linear;
  reconsider Z as Subset-Family of L by A2,XBOOLE_1:1;
  take Y = union Z;
  Y in SF_have b \ SF_have a
  proof
    set X = the Element of Z;
A4: not a in Y
    proof
      assume a in Y;
      then ex X st a in X & X in Z by TARSKI:def 4;
      hence contradiction by A2,Th17;
    end;
    X in SF_have b \ SF_have a by A1,A2;
    then
A5: b in X by Th17;
    then
A6: b in Y by A1,TARSKI:def 4;
    reconsider Y as non empty Subset of L by A1,A5,TARSKI:def 4;
    now
      let p,q be Element of L;
      thus p in Y & q in Y implies p "/\" q in Y
      proof
        assume p in Y;
        then consider X1 such that
A7:     p in X1 and
A8:     X1 in Z by TARSKI:def 4;
A9:     X1 is Filter of L by A2,A8,Th17;
        assume q in Y;
        then consider X2 such that
A10:    q in X2 and
A11:    X2 in Z by TARSKI:def 4;
        X1,X2 are_c=-comparable by A3,A8,A11,ORDINAL1:def 8;
        then
A12:    X1 c= X2 or X2 c= X1;
        X2 is Filter of L by A2,A11,Th17;
        then p "/\" q in X1 or p "/\" q in X2 by A7,A10,A9,A12,FILTER_0:8;
        hence thesis by A8,A11,TARSKI:def 4;
      end;
      assume p "/\" q in Y;
      then consider X1 such that
A13:  p "/\" q in X1 and
A14:  X1 in Z by TARSKI:def 4;
A15:  X1 is Filter of L by A2,A14,Th17;
      then
A16:  q in X1 by A13,FILTER_0:8;
      p in X1 by A13,A15,FILTER_0:8;
      hence p in Y & q in Y by A14,A16,TARSKI:def 4;
    end;
    then Y is Filter of L by FILTER_0:8;
    hence thesis by A4,A6,Lm1;
  end;
  hence thesis by ZFMISC_1:74;
end;

theorem Th19:
  not b [= a implies <.b.) in SF_have b \ SF_have a
proof
  assume not b [= a;
  then not a in <.b.) by FILTER_0:15;
  then
A1: not <.b.) in SF_have a by Th16;
  b in <.b.);
  then <.b.) in SF_have b;
  hence thesis by A1,XBOOLE_0:def 5;
end;

theorem Th20:
  not b [= a implies ex F st F in F_primeSet(L) & not a in F & b in F
proof
  set A = SF_have b \ SF_have a;
  assume not b [= a;
  then
A1: A <> {} by Th19;
  for Z st Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear ex Y st Y
  in SF_have b\ SF_have a & for X1 st X1 in Z holds X1 c= Y by Th18;
  then consider Y such that
A2: Y in A and
A3: for Z st Z in A & Z <> Y holds not Y c= Z by A1,LATTICE4:1;
  reconsider Y as Filter of L by A2,Th17;
A4: b in Y by A2,Th17;
A5: not a in Y by A2,Th17;
A6: Y is prime
  proof
    let a1,a2 be Element of L;
    thus a1"\/"a2 in Y implies a1 in Y or a2 in Y
    proof
      set F2=<.<.a2.) \/ Y.);
      set F1=<.<.a1.) \/ Y.);
      assume that
A7:   a1"\/"a2 in Y and
A8:   not a1 in Y and
A9:   not a2 in Y;
A10:  <.a1.) c= F1 by LATTICE4:2;
      a1 in <.a1.);
      then
A11:  a1 in F1 by A10;
A12:  Y c= F1 by LATTICE4:2;
A13:  <.a2.) c= F2 by LATTICE4:2;
      a2 in <.a2.);
      then
A14:  a2 in F2 by A13;
A15:  Y c= F2 by LATTICE4:2;
      not a in F1 or not a in F2
      proof
        assume that
A16:    a in F1 and
A17:    a in F2;
        consider c1 being Element of L such that
A18:    c1 in Y and
A19:    a1 "/\" c1 [= a by A16,LATTICE4:3;
        consider c2 being Element of L such that
A20:    c2 in Y and
A21:    a2 "/\" c2 [= a by A17,LATTICE4:3;
        set c = c1 "/\" c2;
        a2 "/\" c [= a2 "/\" c2 by LATTICES:6,9;
        then
A22:    a2 "/\" c [= a by A21,LATTICES:7;
        a1 "/\" c [= a1 "/\" c1 by LATTICES:6,9;
        then a1 "/\" c [= a by A19,LATTICES:7;
        then (a1 "/\" c) "\/"( a2 "/\" c) [= a by A22,FILTER_0:6;
        then
A23:    (a1 "\/" a2) "/\" c [= a by LATTICES:def 11;
        c in Y by A18,A20,FILTER_0:8;
        then (a1 "\/" a2) "/\" c in Y by A7,FILTER_0:8;
        hence contradiction by A5,A23,FILTER_0:9;
      end;
      then F1 in A or F2 in A by A4,A12,A15,Lm1;
      hence contradiction by A3,A8,A9,A11,A14,A12,A15;
    end;
    thus thesis by FILTER_0:10;
  end;
  Y <> the carrier of L by A2,Th17;
  then Y in F_primeSet(L) by A6;
  hence thesis by A5,A4;
end;

theorem Th21:
  a <> b implies ex F st F in F_primeSet(L)
proof
  assume a <> b;
  then not a [= b or not b [= a by LATTICES:8;
  then (ex F st F in F_primeSet(L) & not b in F & a in F) or ex F st F in
  F_primeSet(L) & not a in F & b in F by Th20;
  hence thesis;
end;

theorem Th22:
  a <> b implies StoneH(L).a <> StoneH(L).b
proof
  assume a <> b;
  then not a [= b or not b [= a by LATTICES:8;
  then (ex F st F in F_primeSet(L) & not b in F & a in F) or ex F st F in
  F_primeSet(L) & not a in F & b in F by Th20;
  then consider F such that
A1: F in F_primeSet(L) and
A2: b in F & not a in F or a in F & not b in F;
  F in StoneH(L).a & not F in StoneH(L).b or F in StoneH(L).b & not F in
  StoneH(L).a by A1,A2,Th11;
  hence thesis;
end;

registration
  let L;
  cluster StoneH(L) -> one-to-one;
  coherence
proof
  let x1,x2 be object;
  assume that
A1: x1 in dom StoneH(L) and
A2: x2 in dom StoneH(L) and
A3: StoneH(L).x1 = StoneH(L).x2;
  reconsider a1=x1,a2=x2 as Element of L by A1,A2,Def6;
  a1=a2 by A3,Th22;
  hence thesis;
end;
end;

definition
  let L;
  let A,B be Element of StoneS(L);
  redefine func A \/ B -> Element of StoneS(L);  :: redefines \/ (XBOOLE_0, definition)
  coherence
  proof
    consider b such that
A1: B = StoneH(L).b by Th13;
    consider a such that
A2: A = StoneH(L).a by Th13;
    A \/ B = StoneH(L).(a "\/" b) by A2,A1,Th14;
    hence thesis by Th13;
  end;
  redefine func A /\ B -> Element of StoneS(L);  :: redefines /\ (XBOOLE_0, definition)
  coherence
  proof
    consider b such that
A3: B = StoneH(L).b by Th13;
    consider a such that
A4: A = StoneH(L).a by Th13;
    A /\ B = StoneH(L).(a "/\" b) by A4,A3,Th15;
    hence thesis by Th13;
  end;
end;

definition
  let L;
  func Set_Union L -> BinOp of StoneS(L) means
  :Def9:
  for A,B being Element of StoneS(L) holds it.(A,B) = A \/ B;
  existence
  proof
    deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 \/ $2;
    thus ex F being BinOp of StoneS(L) st for P,Q being Element of StoneS(L)
    holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
  end;
  uniqueness
  proof
    set A = StoneS(L);
    deffunc O(Element of A, Element of A) = $1 \/ $2;
    thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
    o2 from BINOP_2:sch 2;
  end;
  func Set_Meet L -> BinOp of StoneS(L) means
  :Def10:
  for A,B being Element of StoneS(L) holds it.(A,B) = A /\ B;
  existence
  proof
    deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 /\ $2;
    thus ex F being BinOp of StoneS(L) st for P,Q being Element of StoneS(L)
    holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
  end;
  uniqueness
  proof
    set A = StoneS(L);
    deffunc O(Element of A, Element of A) = $1 /\ $2;
    thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
    o2 from BINOP_2:sch 2;
  end;
end;

theorem Th23:
  LattStr(#StoneS(L),Set_Union L,Set_Meet L#) is Lattice
proof
  set SL = LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
A1: now
    let p,q be Element of SL;
    thus p "\/" q = q \/ p by Def9
      .= q"\/"p by Def9;
  end;
A2: now
    let p,q be Element of SL;
    thus (p"/\"q)"\/"q = (p"/\"q) \/ q by Def9
      .= (p /\ q) \/ q by Def10
      .= q by XBOOLE_1:22;
  end;
A3: now
    let p,q be Element of SL;
    thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Def10
      .= p /\ (p \/ q) by Def9
      .= p by XBOOLE_1:21;
  end;
A4: now
    let p,q,r be Element of SL;
    thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Def10
      .= p /\ (q /\ r) by Def10
      .= (p /\ q) /\ r by XBOOLE_1:16
      .= (p "/\" q) /\ r by Def10
      .= (p"/\"q)"/\"r by Def10;
  end;
A5: now
    let p,q be Element of SL;
    thus p "/\" q =q /\ p by Def10
      .= q"/\"p by Def10;
  end;
  now
    let p,q,r be Element of SL;
    thus p"\/"(q"\/"r) = p \/ (q "\/" r) by Def9
      .= p \/ (q \/ r) by Def9
      .= (p \/ q) \/ r by XBOOLE_1:4
      .= (p "\/" q) \/ r by Def9
      .= (p"\/"q)"\/"r by Def9;
  end;
  then
  SL is join-commutative join-associative meet-absorbing meet-commutative
  meet-associative join-absorbing by A1,A2,A5,A4,A3;
  hence thesis;
end;

definition
  let L;
  func StoneLatt L -> Lattice equals
  LattStr(#StoneS(L),Set_Union L,Set_Meet L
  #);
  coherence by Th23;
end;

reserve p,q for Element of StoneLatt(L);

theorem
  for L holds the carrier of StoneLatt(L) = StoneS(L);

theorem
  p "\/" q = p \/ q & p "/\" q = p /\ q by Def9,Def10;

theorem
  p [= q iff p c= q
proof
  p "\/" q = p \/ q by Def9;
  hence thesis by XBOOLE_1:7,12;
end;

definition
  let L;
::$N Stone Representation Theorem for Heyting Lattices
  redefine func StoneH(L) -> Homomorphism of L,StoneLatt L;  :: redefines StoneH (OPENLATT, definition)
  coherence
  proof
    dom StoneH(L) = the carrier of L by Def6;
    then reconsider
    f=StoneH(L) as Function of the carrier of L, the carrier of
    StoneLatt L by FUNCT_2:1;
    now
      let a,b;
      thus f.(a "\/" b) = f.(a) \/ f.(b) by Th14
        .=f.a "\/" f.b by Def9;
      thus f.(a "/\" b) = f.(a) /\ f.(b) by Th15
        .=f.(a) "/\" f.(b) by Def10;
    end;
    then f is "\/"-preserving "/\"-preserving;
    hence thesis;
  end;
end;

registration
  let L;
  cluster StoneH(L) -> bijective for Function of L,StoneLatt L;
coherence
proof
  StoneH(L) is one-to-one onto;
  hence thesis;
end;
  cluster StoneLatt(L) -> distributive;
coherence
proof
  StoneH(L) is onto;
  hence thesis by LATTICE4:11;
end;
end;

theorem
  L,StoneLatt L are_isomorphic
proof
  take StoneH(L);
  thus thesis;
end;

registration
  cluster non trivial for H_Lattice;
  existence
  proof
    set T = the non empty TopSpace;
    set OL=Open_setLatt(T);
    the carrier of T = Top OL by Th9;
    then reconsider a= the carrier of T as Element of OL;
    {} = Bottom OL by Th8;
    then reconsider b= {} as Element of OL;
    take OL,a,b;
    thus thesis;
  end;
end;

reserve H for non trivial H_Lattice;
reserve p9,q9 for Element of H;

theorem Th28:
  StoneH(H).(Top H) = F_primeSet(H)
proof
  hereby
    let x be object;
    assume x in StoneH(H).(Top H);
    then
    ex F being Filter of H st F=x & F <> the carrier of H & F is prime
    & Top H in F by Th12;
    hence x in F_primeSet(H);
  end;
  let x be object;
  assume x in F_primeSet(H);
  then consider F being Filter of H such that
A1: F=x and
A2: F <> the carrier of H and
A3: F is prime;
  Top H in F by FILTER_0:11;
  hence thesis by A1,A2,A3,Th12;
end;

theorem Th29:
  StoneH(H).(Bottom H) = {}
proof
  set x = the Element of StoneH(H).(Bottom H);
  assume StoneH(H).(Bottom H) <> {};
  then
  ex F being Filter of H st F=x & F <> the carrier of H & F is prime &
  Bottom H in F by Th12;
  hence contradiction by FILTER_0:26;
end;

theorem Th30:
  StoneS(H) c= bool F_primeSet(H)
proof
  let x be object;
   reconsider xx=x as set by TARSKI:1;
  assume x in StoneS(H);
  then consider p9 such that
A1: x=StoneH(H).p9 by Th13;
A2: x={F where F is Filter of H:F in F_primeSet(H) & p9 in F} by A1,Def6;
  xx c= F_primeSet(H)
  proof
    let y be object;
    assume y in xx;
    then
    ex F being Filter of H st y=F & F in F_primeSet(H) & p9 in F by A2;
    hence thesis;
  end;
  hence thesis;
end;

registration
  let H;
  cluster F_primeSet(H) -> non empty;
  coherence
  proof
    ex p9,q9 st p9 <> q9 by STRUCT_0:def 10;
    then ex F being Filter of H st F in F_primeSet(H) by Th21;
    hence thesis;
  end;
end;

definition
  let H;
  func HTopSpace H -> strict TopStruct means
  :Def12:
  the carrier of it =
F_primeSet(H) & the topology of it =the set of all
union A where A is Subset of StoneS(H);
  existence
  proof
    set FS= F_primeSet(H);
    set top=the set of all union A where A is Subset of StoneS(H);
A1: StoneS(H) c= bool FS by Th30;
    top c= bool FS
    proof
      let x be object;
       reconsider xx=x as set by TARSKI:1;
      assume x in top;
      then consider A being Subset of StoneS(H) such that
A2:   x=union A;
      A c= bool FS by A1;
      then xx c= union bool FS by A2,ZFMISC_1:77;
      then x is Subset of FS by ZFMISC_1:81;
      hence thesis;
    end;
    then reconsider top as Subset-Family of FS;
    take TopStruct(#FS,top#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let H;
  cluster HTopSpace H -> non empty TopSpace-like;
  coherence
  proof
    reconsider A1={StoneH(H).(Top H)} as Subset of StoneS(H);
    set TS = HTopSpace H;
A1: the topology of TS =the set of all union A where A is Subset of StoneS(H)
 by Def12;
A2: the carrier of TS = F_primeSet(H) by Def12;
    hence HTopSpace H is non empty;
    F_primeSet(H) = StoneH(H).(Top H) by Th28;
    then F_primeSet(H)=union A1 by ZFMISC_1:25;
    hence the carrier of TS in the topology of TS by A2,A1;
    hereby
      let a be Subset-Family of TS;
      defpred P[set] means union $1 in a;
      set B= {A where A is Subset of StoneS(H) :P[A]};
      set X= {union A where A is Subset of StoneS(H) : A in B};
      assume
A3:   a c= the topology of TS;
A4:   a = X
      proof
        hereby
          let x be object;
          assume
A5:       x in a;
          then x in the topology of TS by A3;
          then consider A be Subset of StoneS(H) such that
A6:       x=union A by A1;
          A in B by A5,A6;
          hence x in X by A6;
        end;
        let x be object;
        assume x in X;
        then consider A be Subset of StoneS(H) such that
A7:     x=union A and
A8:     A in B;
        ex A9 be Subset of StoneS(H) st A=A9 & union A9 in a by A8;
        hence thesis by A7;
      end;
      reconsider B as Subset-Family of StoneS H from DOMAIN_1:sch 7;
      union union B = union a by A4,EQREL_1:54;
      hence union a in the topology of TS by A1;
    end;
    let a,b be Subset of TS;
    assume that
A9: a in the topology of TS and
A10: b in the topology of TS;
    consider A being Subset of StoneS(H) such that
A11: a = union A by A1,A9;
    consider B being Subset of StoneS(H) such that
A12: b = union B by A1,A10;
    INTERSECTION(A,B) c= StoneS(H)
    proof
      let x be object;
      assume x in INTERSECTION(A,B);
      then consider X,Y being set such that
A13:  X in A and
A14:  Y in B and
A15:  x = X /\ Y by SETFAM_1:def 5;
      consider p9 such that
A16:  X=StoneH(H).p9 by A13,Th13;
      consider q9 such that
A17:  Y=StoneH(H).q9 by A14,Th13;
      x = StoneH(H).(p9 "/\" q9) by A15,A16,A17,Th15;
      hence thesis;
    end;
    then reconsider C=INTERSECTION(A,B) as Subset of StoneS(H);
    union A /\ union B = union C by SETFAM_1:28;
    hence thesis by A1,A11,A12;
  end;
end;

theorem
  the carrier of Open_setLatt(HTopSpace H) = the set of all
union A where A is Subset
  of StoneS(H) by Def12;

theorem Th32:
  StoneS(H) c= the carrier of Open_setLatt(HTopSpace H)
proof
  let x be object;
  set carrO = the carrier of Open_setLatt(HTopSpace H);
  assume x in StoneS(H);
  then reconsider z={x} as Subset of StoneS(H) by ZFMISC_1:31;
A1: union z = x by ZFMISC_1:25;
  carrO = the set of all union A where A is Subset of StoneS(H) by Def12;
  hence thesis by A1;
end;

definition
  let H;
  redefine func StoneH(H) -> Homomorphism of H,Open_setLatt(HTopSpace H);  :: redefines StoneH (OPENLATT, definition)
  coherence
  proof
    set LH=Open_setLatt(HTopSpace H);
    reconsider g=StoneH(H) as Function of the carrier of H, the carrier of
    StoneLatt(H);
    StoneS(H) c= the carrier of LH by Th32;
    then reconsider f=g as Function of the carrier of H, the carrier of LH by
FUNCT_2:6;
    now
      let p9,q9;
      thus f.(p9 "\/" q9) = StoneH(H).p9 \/ StoneH(H).q9 by Th14
        .= f.p9 "\/" f.q9 by Def2;
      thus f.(p9 "/\" q9) = StoneH(H).p9 /\ StoneH(H).q9 by Th15
        .= f.p9 "/\" f.q9 by Def3;
    end;
    then f is "\/"-preserving "/\"-preserving;
    hence thesis;
  end;
end;

theorem Th33:
  StoneH(H).(p9 => q9) = (StoneH(H).p9) => (StoneH(H).q9)
proof
A1: the carrier of Open_setLatt(HTopSpace H) = the set of all
union A where A is Subset of
  StoneS(H) by Def12;
A2: now
    let r be Element of Open_setLatt(HTopSpace H);
    r in the carrier of Open_setLatt(HTopSpace H);
    then consider A being Subset of StoneS(H) such that
A3: r = union A by A1;
    assume StoneH(H).p9 "/\" r [= StoneH(H).q9;
    then StoneH(H).p9 "/\" r c= StoneH(H).q9 by Th6;
    then StoneH(H).p9 /\ union A c= StoneH(H).q9 by A3,Def3;
    then
A4: union INTERSECTION ({StoneH(H).p9}, A) c= StoneH(H).q9 by SETFAM_1:25;
    now
      let x;
      assume
A5:   x in A;
      then consider x9 being Element of H such that
A6:   x=StoneH(H).x9 by Th13;
      StoneH(H).p9 in {StoneH(H).p9} by TARSKI:def 1;
      then StoneH(H).p9 /\ x in INTERSECTION ({StoneH(H).p9}, A) by A5,
SETFAM_1:def 5;
      then StoneH(H).p9 /\ StoneH(H).x9 c= StoneH(H).q9 by A4,A6,SETFAM_1:41;
      then StoneH(H).(p9 "/\" x9) c= StoneH(H).q9 by Th15;
      then StoneH(H).(p9 "/\" x9) [= StoneH(H).q9 by Th6;
      then (p9 "/\" x9) [= q9 by LATTICE4:5;
      then x9 [= p9 => q9 by FILTER_0:def 7;
      then StoneH(H).x9 [= StoneH(H).(p9 => q9) by LATTICE4:4;
      hence x c= StoneH(H).(p9 => q9) by A6,Th6;
    end;
    then union A c= StoneH(H).(p9 => q9) by ZFMISC_1:76;
    hence r [= StoneH(H).(p9 => q9) by A3,Th6;
  end;
  p9 "/\" (p9 => q9) [= q9 by FILTER_0:def 7;
  then StoneH(H).(p9 "/\" (p9 => q9)) [= StoneH(H).q9 by LATTICE4:4;
  then StoneH(H).p9"/\" StoneH(H).(p9 => q9) [= StoneH(H).q9
  by LATTICE4:def 2;
  hence thesis by A2,FILTER_0:def 7;
end;

theorem
  StoneH(H) preserves_implication
by Th33;

theorem
  StoneH(H) preserves_top
proof
  StoneH(H).(Top H) = F_primeSet(H) by Th28
    .= the carrier of HTopSpace H by Def12
    .= Top (Open_setLatt(HTopSpace H)) by Th9;
  hence thesis;
end;

theorem
  StoneH(H) preserves_bottom
proof
  StoneH(H).(Bottom H) = {} by Th29
    .= Bottom (Open_setLatt(HTopSpace H)) by Th8;
  hence thesis;
end;