:: Galois Connections
::  by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2021 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 XBOOLE_0, STRUCT_0, FUNCT_1, SUBSET_1, ORDERS_2, SEQM_3,
      XXREAL_0, RELAT_2, LATTICE3, LATTICES, EQREL_1, WAYBEL_0, YELLOW_1,
      YELLOW_0, RELAT_1, CAT_1, WELLORD1, ORDINAL2, TARSKI, REWRITE1, CARD_FIL,
      BINOP_1, FUNCT_2, GROUP_6, YELLOW_2, LATTICE2, XBOOLEAN, ZFMISC_1,
      XXREAL_2, WAYBEL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, QUANTAL1, ORDERS_3,
      YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2;
 constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, RELSET_1;
 registrations RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_1, YELLOW_2, RELSET_1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

definition
  let L1,L2 be non empty 1-sorted, f be Function of L1,L2;
  redefine attr f is one-to-one means
:: WAYBEL_1:def 1
  for x,y being Element of L1 st f.x = f.y holds x=y;
end;

definition
  let L1,L2 be non empty RelStr, f be Function of L1,L2;
  redefine attr f is monotone means
:: WAYBEL_1:def 2

  for x,y being Element of L1 st x <= y holds f.x <= f.y;
end;

theorem :: WAYBEL_1:1
  for L being antisymmetric transitive with_infima RelStr, x,y,z
  being Element of L st x <= y holds x "/\" z <= y "/\" z;

theorem :: WAYBEL_1:2
  for L being antisymmetric transitive with_suprema RelStr, x,y,z
  being Element of L st x <= y holds x "\/" z <= y "\/" z;

theorem :: WAYBEL_1:3
  for L being non empty lower-bounded antisymmetric RelStr for x
being Element of L holds (L is with_infima implies Bottom L "/\" x = Bottom L)
  & (L is with_suprema reflexive transitive implies Bottom L "\/" x = x);

theorem :: WAYBEL_1:4
  for L being non empty upper-bounded antisymmetric RelStr for x
  being Element of L holds (L is with_infima transitive reflexive implies Top L
  "/\" x = x) & (L is with_suprema implies Top L "\/" x = Top L);

definition
  let L be non empty RelStr;
  attr L is distributive means
:: WAYBEL_1:def 3

  for x,y,z being Element of L holds x
  "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);
end;

theorem :: WAYBEL_1:5
  for L being LATTICE holds L is distributive iff for x,y,z being
  Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z);

registration
  let X be set;
  cluster BoolePoset X -> distributive;
end;

definition
  let S be non empty RelStr, X be set;
  pred ex_min_of X,S means
:: WAYBEL_1:def 4
  ex_inf_of X,S & "/\"(X,S) in X;
  pred ex_max_of X,S means
:: WAYBEL_1:def 5

  ex_sup_of X,S & "\/"(X,S) in X;
end;

notation
  let S be non empty RelStr, X be set;
  synonym X has_the_min_in S for ex_min_of X,S;
  synonym X has_the_max_in S for ex_max_of X,S;
end;

definition
  let S be non empty RelStr, s be Element of S, X be set;
  pred s is_minimum_of X means
:: WAYBEL_1:def 6

  ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S ) in X;
  pred s is_maximum_of X means
:: WAYBEL_1:def 7

  ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S )in X;
end;

registration
  let L be RelStr;
  cluster id L -> isomorphic;
end;

definition
  let L1,L2 be RelStr;
  pred L1,L2 are_isomorphic means
:: WAYBEL_1:def 8

  ex f being Function of L1,L2 st f is isomorphic;
  reflexivity;
end;

theorem :: WAYBEL_1:6
  for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds L2,L1
  are_isomorphic;

theorem :: WAYBEL_1:7
  for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic
  holds L1,L3 are_isomorphic;

begin :: Galois Connections

definition
  let S,T be RelStr;
  mode Connection of S,T -> set means
:: WAYBEL_1:def 9

    ex g being Function of S,T, d being Function of T,S st it = [g,d];
end;

definition
  let S,T be RelStr, g be Function of S,T, d be Function of T,S;
  redefine func [g,d] -> Connection of S,T;
end;

:: Definition 3.1

definition
  let S,T be non empty RelStr, gc be Connection of S,T;
  attr gc is Galois means
:: WAYBEL_1:def 10

  ex g being Function of S,T, d being Function
of T,S st gc = [g,d] & g is monotone & d is monotone & for t being Element of T
  , s being Element of S holds t <= g.s iff d.t <= s;
end;

theorem :: WAYBEL_1:8
  for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S holds [g,d] is Galois iff g is monotone & d is monotone & for t
  being Element of T, s being Element of S holds t <= g.s iff d.t <= s;

:: Definition 3.1

definition
  let S,T be non empty RelStr, g be Function of S,T;
  attr g is upper_adjoint means
:: WAYBEL_1:def 11

  ex d being Function of T,S st [g,d] is Galois;
end;

:: Definition 3.1

definition
  let S,T be non empty RelStr, d be Function of T,S;
  attr d is lower_adjoint means
:: WAYBEL_1:def 12

  ex g being Function of S,T st [g,d] is Galois;
end;

theorem :: WAYBEL_1:9
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st [g,d] is Galois holds g is upper_adjoint & d is
  lower_adjoint;

:: Theorem 3.2  (1) iff (2)

theorem :: WAYBEL_1:10
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S holds [g,d] is Galois iff g is monotone & for t being Element
  of T holds d.t is_minimum_of g"(uparrow t);

:: Theorem 3.2 (1) iff (3)

theorem :: WAYBEL_1:11
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S holds [g,d] is Galois iff d is monotone & for s being Element
  of S holds g.s is_maximum_of d"(downarrow s);

:: Theorem 3.3 (first part)

theorem :: WAYBEL_1:12
  for S,T being non empty Poset,g being Function of S,T st g is
  upper_adjoint holds g is infs-preserving;

registration
  let S,T be non empty Poset;
  cluster upper_adjoint -> infs-preserving for Function of S,T;
end;

:: Theorem 3.3 (second part)

theorem :: WAYBEL_1:13
  for S,T being non empty Poset, d being Function of T,S st d is
  lower_adjoint holds d is sups-preserving;

registration
  let S,T be non empty Poset;
  cluster lower_adjoint -> sups-preserving for Function of S,T;
end;

:: Theorem 3.4

theorem :: WAYBEL_1:14
  for S,T being non empty Poset,g being Function of S,T st S is
complete & g is infs-preserving ex d being Function of T,S st [g,d] is Galois &
  for t being Element of T holds d.t is_minimum_of g"(uparrow t);

:: Theorem 3.4 (dual)

theorem :: WAYBEL_1:15
  for S,T being non empty Poset, d being Function of T,S st T is
complete & d is sups-preserving ex g being Function of S,T st [g,d] is Galois &
  for s being Element of S holds g.s is_maximum_of d"(downarrow s);

:: Corollary 3.5 (i)

theorem :: WAYBEL_1:16
  for S,T being non empty Poset, g being Function of S,T st S is
  complete holds (g is infs-preserving iff g is monotone & g is upper_adjoint);

:: Corollary 3.5 (ii)

theorem :: WAYBEL_1:17
  for S,T being non empty Poset, d being Function of T,S st T is
  complete holds d is sups-preserving iff d is monotone & d is lower_adjoint;

:: Theorem 3.6 (1) iff (2)

theorem :: WAYBEL_1:18
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st [g,d] is Galois holds d*g <= id S & id T <= g*d;

:: Theorem 3.6 (2) implies (1)

theorem :: WAYBEL_1:19
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d
  holds [g,d] is Galois;

:: Theorem 3.6 (2) implies (3)

theorem :: WAYBEL_1:20
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d
  holds d = d*g*d & g = g*d*g;

:: Theorem 3.6 (3) implies (4)

theorem :: WAYBEL_1:21
  for S,T being non empty RelStr, g being Function of S,T, d being
  Function of T,S st g = g*d*g holds g*d is idempotent;

:: Proposition 3.7 (1) implies (2)

theorem :: WAYBEL_1:22
  for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S st [g,d] is Galois & g is onto for t being Element of T holds d
  .t is_minimum_of g"{t};

:: Proposition 3.7 (2) implies (3)

theorem :: WAYBEL_1:23
  for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S st for t being Element of T holds d.t is_minimum_of g"{t} holds
  g*d = id T;

:: Proposition 3.7 (4) iff (1)

theorem :: WAYBEL_1:24
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st [g,d] is Galois holds g is onto iff d is one-to-one;

:: Proposition 3.7 (1*) implies (2*)

theorem :: WAYBEL_1:25
  for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S st [g,d] is Galois & d is onto for s being Element of S holds g
  .s is_maximum_of d"{s};

:: Proposition 3.7 (2*) implies (3*)

theorem :: WAYBEL_1:26
  for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S st for s being Element of S holds g.s is_maximum_of d"{s} holds
  d*g = id S;

:: Proposition 3.7 (1*) iff (4*)

theorem :: WAYBEL_1:27
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st [g,d] is Galois holds g is one-to-one iff d is onto;

:: Definition 3.8 (i)

definition
  let L be non empty RelStr, p be Function of L,L;
  attr p is projection means
:: WAYBEL_1:def 13

  p is idempotent monotone;
end;

registration
  let L be non empty RelStr;
  cluster id L -> projection;
end;

registration
  let L be non empty RelStr;
  cluster projection for Function of L,L;
end;

:: Definition 3.8 (ii)

definition
  let L be non empty RelStr, c be Function of L,L;
  attr c is closure means
:: WAYBEL_1:def 14

  c is projection & id(L) <= c;
end;

registration
  let L be non empty RelStr;
  cluster closure -> projection for Function of L,L;
end;

registration
  let L be non empty reflexive RelStr;
  cluster closure for Function of L,L;
end;

registration
  let L be non empty reflexive RelStr;
  cluster id L -> closure;
end;

:: Definition 3.8 (iii)

definition
  let L be non empty RelStr, k be Function of L,L;
  attr k is kernel means
:: WAYBEL_1:def 15

  k is projection & k <= id(L);
end;

registration
  let L be non empty RelStr;
  cluster kernel -> projection for Function of L,L;
end;

registration
  let L be non empty reflexive RelStr;
  cluster kernel for Function of L,L;
end;

registration
  let L be non empty reflexive RelStr;
  cluster id L -> kernel;
end;

theorem :: WAYBEL_1:28
  for L being non empty Poset, c being Function of L,L, X being
Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X
  );

theorem :: WAYBEL_1:29
  for L being non empty Poset, k being Function of L,L, X being
Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k.(sup X)
;

definition
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  func corestr(g) -> Function of L1,Image g equals
:: WAYBEL_1:def 16
  (the carrier of Image g)|`g;
end;

theorem :: WAYBEL_1:30
  for L1, L2 being non empty RelStr,g being Function of L1,L2
  holds corestr g = g;

registration
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  cluster corestr g -> onto;
end;

theorem :: WAYBEL_1:31
  for L1, L2 being non empty RelStr, g being Function of L1,L2 st
  g is monotone holds corestr g is monotone;

definition
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  func inclusion(g) -> Function of Image g,L2 equals
:: WAYBEL_1:def 17
  id Image g;
end;

registration
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  cluster inclusion g -> one-to-one monotone;
end;

theorem :: WAYBEL_1:32
  for L being non empty RelStr, f being Function of L,L holds (
  inclusion f)*(corestr f) = f;

::Theorem 3.10 (1) implies (2)

theorem :: WAYBEL_1:33
  for L being non empty Poset, f being Function of L,L st f is
  idempotent holds (corestr f)*(inclusion f) = id(Image f);

::Theorem 3.10 (1) implies (3)

theorem :: WAYBEL_1:34
  for L being non empty Poset, f being Function of L,L st f is
  projection ex T being non empty Poset, q being Function of L,T, i being
Function of T,L st q is monotone & q is onto & i is monotone & i is one-to-one
  & f = i*q & id(T) = q*i;

::Theorem 3.10 (3) implies (1)

theorem :: WAYBEL_1:35
  for L being non empty Poset, f being Function of L,L st (ex T being
  non empty Poset, q being Function of L,T, i being Function of T,L st q is
  monotone & i is monotone & f = i*q & id(T) = q*i) holds f is projection;

::Theorem 3.10 (1_1) implies (2_1)

theorem :: WAYBEL_1:36
  for L being non empty Poset, f being Function of L,L st f is
  closure holds [inclusion f,corestr f] is Galois;

::Theorem 3.10 (2_1) implies (3_1)

theorem :: WAYBEL_1:37
  for L being non empty Poset, f being Function of L,L st f is closure
ex S being non empty Poset, g being Function of S,L, d being Function of L,S st
  [g,d] is Galois & f = g*d;

::Theorem 3.10 (3_1) implies (1_1)

theorem :: WAYBEL_1:38
  for L being non empty Poset, f being Function of L,L st f is
  monotone & ex S being non empty Poset, g being Function of S,L, d being
  Function of L,S st [g,d] is Galois & f = g*d holds f is closure;

::Theorem 3.10 (1_2) implies (2_2)

theorem :: WAYBEL_1:39
  for L being non empty Poset, f being Function of L,L st f is
  kernel holds [corestr f,inclusion f] is Galois;

::Theorem 3.10 (2_2) implies (3_2)

theorem :: WAYBEL_1:40
  for L being non empty Poset, f being Function of L,L st f is kernel ex
T being non empty Poset, g being Function of L,T, d being Function of T,L st [g
  ,d] is Galois & f = d*g;

::Theorem 3.10 (3_2) implies (1_2)

theorem :: WAYBEL_1:41
  for L being non empty Poset, f being Function of L,L st f is monotone
& ex T being non empty Poset, g being Function of L,T, d being Function of T,L
  st [g,d] is Galois & f = d*g holds f is kernel;

:: Lemma 3.11 (i) (part I)

theorem :: WAYBEL_1:42
  for L being non empty Poset, p being Function of L,L st p is
projection holds rng p = {c where c is Element of L: c <= p.c} /\ {k where k is
  Element of L: p.k <= k};

theorem :: WAYBEL_1:43
  for L being non empty Poset, p being Function of L,L st p is
projection holds {c where c is Element of L: c <= p.c} is non empty Subset of L
  & {k where k is Element of L: p.k <= k} is non empty Subset of L;

:: Lemma 3.11 (i) (part II)

theorem :: WAYBEL_1:44
  for L being non empty Poset, p being Function of L,L st p is
projection holds rng(p|{c where c is Element of L: c <= p.c}) = rng p & rng(p|{
  k where k is Element of L: p.k <= k}) = rng p;

theorem :: WAYBEL_1:45
  for L being non empty Poset, p being Function of L,L st p is
  projection for Lc being non empty Subset of L, Lk being non empty Subset of L
  st Lc = {c where c is Element of L: c <= p.c} holds p|Lc is Function of
  subrelstr Lc,subrelstr Lc;

theorem :: WAYBEL_1:46
  for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} holds p|Lk is Function of subrelstr Lk,subrelstr Lk;

:: Lemma 3.11 (i) (part IIIa)

theorem :: WAYBEL_1:47
  for L being non empty Poset, p being Function of L,L st p is
projection for Lc being non empty Subset of L st Lc = {c where c is Element of
L: c <= p.c} for pc being Function of subrelstr Lc,subrelstr Lc st pc = p|Lc
  holds pc is closure;

:: Lemma 3.11 (i) (part IIIb)

theorem :: WAYBEL_1:48
  for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} for pk being Function of subrelstr Lk,subrelstr Lk st pk = p|Lk
  holds pk is kernel;

:: Lemma 3.11 (ii) (part I)

theorem :: WAYBEL_1:49
  for L being non empty Poset, p being Function of L,L st p is
monotone for Lc being Subset of L st Lc = {c where c is Element of L: c <= p.c}
  holds subrelstr Lc is sups-inheriting;

:: Lemma 3.11 (ii) (part II)

theorem :: WAYBEL_1:50
  for L being non empty Poset, p being Function of L,L st p is
monotone for Lk being Subset of L st Lk = {k where k is Element of L: p.k <= k}
  holds subrelstr Lk is infs-inheriting;

:: Lemma 3.11 (iii) (part I)

theorem :: WAYBEL_1:51
  for L being non empty Poset, p being Function of L,L st p is
projection for Lc being non empty Subset of L st Lc = {c where c is Element of
L: c <= p.c} holds (p is infs-preserving implies subrelstr Lc is
infs-inheriting & Image p is infs-inheriting) & (p is filtered-infs-preserving
  implies subrelstr Lc is filtered-infs-inheriting & Image p is
  filtered-infs-inheriting);

:: Lemma 3.11 (iii) (part II)

theorem :: WAYBEL_1:52
  for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} holds (p is sups-preserving implies subrelstr Lk is
sups-inheriting & Image p is sups-inheriting) & (p is directed-sups-preserving
  implies subrelstr Lk is directed-sups-inheriting & Image p is
  directed-sups-inheriting);

:: Proposition 3.12 (i)

theorem :: WAYBEL_1:53
  for L being non empty Poset, p being Function of L,L holds (p is
  closure implies Image p is infs-inheriting) & (p is kernel implies Image p is
  sups-inheriting);

:: Proposition 3.12 (ii)

theorem :: WAYBEL_1:54
  for L being complete non empty Poset, p being Function of L,L st p
  is projection holds Image p is complete;

:: Proposition 3.12 (iii)

theorem :: WAYBEL_1:55
  for L being non empty Poset, c being Function of L,L st c is closure
  holds corestr c is sups-preserving & for X being Subset of L st X c= the
carrier of Image c & ex_sup_of X,L holds ex_sup_of X,Image c & "\/"(X,Image c)
  = c.("\/"(X,L));

:: Proposition 3.12 (iv)

theorem :: WAYBEL_1:56
  for L being non empty Poset, k being Function of L,L st k is kernel
  holds (corestr k) is infs-preserving & for X being Subset of L st X c= the
carrier of Image k & ex_inf_of X,L holds ex_inf_of X,Image k & "/\"(X,Image k)
  = k.("/\"(X,L));

begin :: Heyting algebras
:: Proposition 3.15 (i)

theorem :: WAYBEL_1:57
  for L being complete non empty Poset holds [IdsMap L,SupMap L]
  is Galois & SupMap L is sups-preserving;

:: Proposition 3.15 (ii)

theorem :: WAYBEL_1:58
  for L being complete non empty Poset holds (IdsMap L)*(SupMap L) is
  closure & Image ((IdsMap L)*(SupMap L)),L are_isomorphic;

definition
  let S be non empty RelStr;
  let x be Element of S;
  func x "/\" -> Function of S,S means
:: WAYBEL_1:def 18

  for s being Element of S holds it.s = x"/\"s;
end;

theorem :: WAYBEL_1:59
  for S being non empty RelStr, x,t being Element of S holds {s
  where s is Element of S: x"/\"s <= t} = (x "/\")"(downarrow t);

theorem :: WAYBEL_1:60
  for S being Semilattice, x be Element of S holds x "/\" is monotone;

registration
  let S be Semilattice, x be Element of S;
  cluster x "/\" -> monotone;
end;

theorem :: WAYBEL_1:61
  for S being non empty RelStr, x being Element of S, X being
  Subset of S holds (x "/\").:X = {x"/\"y where y is Element of S: y in X};

:: Lemma 3.16 (1) iff (2)

theorem :: WAYBEL_1:62
  for S being Semilattice holds (for x being Element of S holds x
"/\" is lower_adjoint) iff for x,t being Element of S holds ex_max_of {s where
  s is Element of S: x"/\"s <= t},S;

:: Lemma 3.16 (1) implies (3)

theorem :: WAYBEL_1:63
  for S being Semilattice st for x being Element of S holds x "/\"
  is lower_adjoint for X being Subset of S st ex_sup_of X,S for x being Element
of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S);

:: Lemma 3.16 (1) iff (3)

theorem :: WAYBEL_1:64
  for S being complete non empty Poset holds (for x being Element of S
holds x "/\" is lower_adjoint) iff for X being Subset of S, x being Element of
  S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S);

:: Lemma 3.16 (3) implies (D)

theorem :: WAYBEL_1:65
  for S being LATTICE st for X being Subset of S st ex_sup_of X,S
  for x being Element of S holds x"/\"("\/"(X,S)) = "\/"({x"/\" y where y is
  Element of S: y in X},S) holds S is distributive;

definition
  let H be non empty RelStr;
  attr H is Heyting means
:: WAYBEL_1:def 19

  H is LATTICE & for x being Element of H holds x "/\" is lower_adjoint;
end;

registration
  cluster Heyting -> with_infima with_suprema reflexive transitive
    antisymmetric for non empty RelStr;
end;

definition
  let H be non empty RelStr, a be Element of H;
  assume
 H is Heyting;
  func a => -> Function of H,H means
:: WAYBEL_1:def 20

  [it,a "/\"] is Galois;
end;

theorem :: WAYBEL_1:66
  for H being non empty RelStr st H is Heyting holds H is distributive;

registration
  cluster Heyting -> distributive for non empty RelStr;
end;

definition
  let H be non empty RelStr, a,y be Element of H;
  func a => y -> Element of H equals
:: WAYBEL_1:def 21
  (a=>).y;
end;

theorem :: WAYBEL_1:67
  for H being non empty RelStr st H is Heyting for x,a,y being
  Element of H holds x >= a "/\" y iff a => x >= y;

theorem :: WAYBEL_1:68
  for H being non empty RelStr st H is Heyting holds H is upper-bounded;

registration
  cluster Heyting -> upper-bounded for non empty RelStr;
end;

theorem :: WAYBEL_1:69
  for H being non empty RelStr st H is Heyting for a,b being
  Element of H holds Top H = a => b iff a <= b;

theorem :: WAYBEL_1:70
  for H being non empty RelStr st H is Heyting for a being Element of H
  holds Top H = a => a;

theorem :: WAYBEL_1:71
  for H being non empty RelStr st H is Heyting for a,b being Element of
  H st Top H = a => b & Top H = b => a holds a = b;

theorem :: WAYBEL_1:72
  for H being non empty RelStr st H is Heyting for a,b being
  Element of H holds b <= (a => b);

theorem :: WAYBEL_1:73
  for H being non empty RelStr st H is Heyting for a being Element of H
  holds Top H = a => Top H;

theorem :: WAYBEL_1:74
  for H being non empty RelStr st H is Heyting for b being Element of H
  holds b = (Top H) => b;

theorem :: WAYBEL_1:75
  for H being non empty RelStr st H is Heyting for a,b,c being
  Element of H st a <= b holds (b => c) <= (a => c);

theorem :: WAYBEL_1:76
  for H being non empty RelStr st H is Heyting for a,b,c being Element
  of H st b <= c holds (a => b) <= (a => c);

theorem :: WAYBEL_1:77
  for H being non empty RelStr st H is Heyting for a,b being
  Element of H holds a"/\"(a => b) = a"/\"b;

theorem :: WAYBEL_1:78
  for H being non empty RelStr st H is Heyting for a,b,c being
  Element of H holds (a"\/"b)=> c = (a => c) "/\" (b => c);

definition
  let H be non empty RelStr, a be Element of H;
  func 'not' a -> Element of H equals
:: WAYBEL_1:def 22
  a => Bottom H;
end;

theorem :: WAYBEL_1:79
  for H being non empty RelStr st H is Heyting & H is lower-bounded for
a being Element of H holds 'not' a is_maximum_of {x where x is Element of H: a
  "/\"x = Bottom H};

theorem :: WAYBEL_1:80
  for H being non empty RelStr st H is Heyting & H is
  lower-bounded holds 'not' Bottom H = Top H & 'not' Top H = Bottom H;

:: Exercise 3.18 (i)

theorem :: WAYBEL_1:81
  for H being non empty lower-bounded RelStr st H is Heyting for a,b
  being Element of H holds 'not' a >= b iff 'not' b >= a;

:: Exercise 3.18 (ii)

theorem :: WAYBEL_1:82
  for H being non empty lower-bounded RelStr st H is Heyting for a
  ,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H;

theorem :: WAYBEL_1:83
  for H being non empty lower-bounded RelStr st H is Heyting for a,b
  being Element of H st a <= b holds 'not' b <= 'not' a;

theorem :: WAYBEL_1:84
  for H being non empty lower-bounded RelStr st H is Heyting for a,b
  being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b;

theorem :: WAYBEL_1:85
  for H being non empty lower-bounded RelStr st H is Heyting for a,b
  being Element of H holds 'not' (a"/\"b) >= 'not' a"\/"'not' b;

definition
  let L be non empty RelStr, x,y be Element of L;
  pred y is_a_complement_of x means
:: WAYBEL_1:def 23

  x "\/" y = Top L & x "/\" y = Bottom L;
end;

definition
  let L be non empty RelStr;
  attr L is complemented means
:: WAYBEL_1:def 24

  for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;

registration
  let X be set;
  cluster BoolePoset X -> complemented;
end;

:: Exercise 3.19

theorem :: WAYBEL_1:86
  for L being bounded LATTICE st L is Heyting & for x being
  Element of L holds 'not' 'not' x = x for x being Element of L holds 'not' x
  is_a_complement_of x;

:: Exercise 3.19  (1) iff (2)

theorem :: WAYBEL_1:87
  for L being bounded LATTICE holds L is distributive complemented
  iff L is Heyting & for x being Element of L holds 'not' 'not' x = x;

:: Definition 3.20

definition
  let B be non empty RelStr;
  attr B is Boolean means
:: WAYBEL_1:def 25

  B is LATTICE & B is bounded distributive complemented;
end;

registration
  cluster Boolean -> reflexive transitive antisymmetric with_infima
    with_suprema bounded distributive complemented for non empty RelStr;
end;

registration
  cluster reflexive transitive antisymmetric with_infima with_suprema bounded
    distributive complemented -> Boolean for non empty RelStr;
end;

registration
  cluster Boolean -> Heyting for non empty RelStr;
end;

registration
  cluster strict Boolean non empty for LATTICE;
end;

registration
  cluster strict Heyting non empty for LATTICE;
end;