BOOLEALG

:: Boolean Properties of Lattices
::  by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-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 LATTICES, SUBSET_1, XBOOLE_0, EQREL_1, PBOOLE;
 notations STRUCT_0, LATTICES;
 constructors LATTICES;
 registrations LATTICES;
 theorems LATTICES, FILTER_0, LATTICE4;

begin :: General Lattices

reserve L for Lattice;
reserve X,Y,Z,V for Element of L;

definition
  let L,X,Y;
  func X \ Y -> Element of L equals
  X "/\" Y`;
  coherence;
end;

definition
  let L,X,Y;
  func X \+\ Y -> Element of L equals
  (X \ Y) "\/" (Y \ X);
  coherence;
end;

definition
  let L,X,Y;
  redefine pred X = Y means  :: redefines = (HIDDEN, definition)

  X [= Y & Y [= X;
  compatibility by LATTICES:8;
end;

definition
  let L,X,Y;
  pred X meets Y means

  X "/\" Y <> Bottom L;
end;

notation
  let L,X,Y;
  antonym X misses Y for X meets Y;
end;

theorem
  X "\/" Y [= Z implies X [= Z
proof
  assume X "\/" Y [= Z;
  then X "/\" (X "\/" Y) [= X "/\" Z by LATTICES:9;
  then
A1: X [= X "/\" Z by LATTICES:def 9;
  X "/\" Z [= Z by LATTICES:6;
  hence thesis by A1,LATTICES:7;
end;

theorem
  X "/\" Y [= X "\/" Z
proof
  X "/\" Y [= X & X [= X "\/" Z by LATTICES:5,6;
  hence thesis by LATTICES:7;
end;

theorem
  X [= Z implies X \ Y [= Z
proof
  assume X [= Z;
  then
A1: X "/\" Y` [= Z "/\" Y` by LATTICES:9;
  Z "/\" Y` [= Z by LATTICES:6;
  hence thesis by A1,LATTICES:7;
end;

theorem
  X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z by FILTER_0:6;

theorem
  X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V
proof
  thus X = Y "\/" Z implies Y [= X & Z [= X & for V st Y [= V & Z [= V holds X
  [= V by FILTER_0:6,LATTICES:5;
  assume that
A1: Y [= X & Z [= X and
A2: for V st Y [= V & Z [= V holds X [= V;
A3: Y "\/" Z [= X by A1,FILTER_0:6;
  Y [= Y "\/" Z & Z [= Y "\/" Z by LATTICES:5;
  then X [= Y "\/" Z by A2;
  hence thesis by A3;
end;

theorem
  X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X
proof
  thus X = Y "/\" Z implies X [= Y & X [= Z & for V st V [= Y & V [= Z holds V
  [= X by FILTER_0:7,LATTICES:6;
  assume that
A1: X [= Y & X [= Z and
A2: for V st V [= Y & V [= Z holds V [= X;
A3: X [= Y "/\" Z by A1,FILTER_0:7;
  Y "/\" Z [= Y & Y "/\" Z [= Z by LATTICES:6;
  then Y "/\" Z [= X by A2;
  hence thesis by A3;
end;

theorem
  X meets X iff X <> Bottom L;

definition
  let L, X, Y;
  redefine pred X meets Y;  :: redefines meets (BOOLEALG, definition)
  symmetry;
  redefine func X \+\ Y;  :: redefines \+\ (BOOLEALG, definition)
  commutativity;
  redefine pred X misses Y;  :: redefines misses (BOOLEALG, antonym) → meets (BOOLEALG, definition)
  symmetry;
end;

begin

begin :: Distributive Lattices

reserve L for D_Lattice;
reserve X,Y,Z for Element of L;

theorem
  (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z
proof
  assume (X "/\" Y) "\/" (X "/\" Z) = X;
  then X "/\" (Y "\/" Z) = X by LATTICES:def 11;
  hence thesis by LATTICES:4;
end;

begin :: Distributive Bounded Lattices

reserve L for 0_Lattice;
reserve X,Y,Z for Element of L;

theorem Th9:
  X [= Bottom L implies X = Bottom L
by LATTICES:16;

theorem
  X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L by Th9,FILTER_0:7;

theorem Th11:
  X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L
by LATTICES:5,LATTICES:16;

theorem
  X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L by Th9,LATTICES:9;

theorem Th13:
  X meets Y & Y [= Z implies X meets Z
by Th9,LATTICES:9;

theorem Th14:
  X meets Y "/\" Z implies X meets Y & X meets Z
proof
  assume X meets Y "/\" Z;
  then
A1: X "/\" (Y "/\" Z) <> Bottom L;
  then X "/\" Z "/\" Y <> Bottom L by LATTICES:def 7;
  then
A2: X "/\" Z <> Bottom L;
  X "/\" Y "/\" Z <> Bottom L by A1,LATTICES:def 7;
  then X "/\" Y <> Bottom L;
  hence thesis by A2;
end;

theorem
  X meets Y \ Z implies X meets Y
proof
  assume X meets Y \ Z;
  then X "/\" (Y \ Z) <> Bottom L;
  then X "/\" Y "/\" Z` <> Bottom L by LATTICES:def 7;
  then X "/\" Y <> Bottom L;
  hence thesis;
end;

theorem
  X misses Bottom L;

theorem
  X misses Z & Y [= Z implies X misses Y by Th13;

theorem
  X misses Y or X misses Z implies X misses Y "/\" Z by Th14;

theorem
  X [= Y & X [= Z & Y misses Z implies X = Bottom L
by Th9,FILTER_0:7;

theorem
  X misses Y implies (Z "/\" X) misses (Z "/\" Y)
proof
  assume
A1: X misses Y;
  (Z "/\" X) "/\" (Z "/\" Y) = Z "/\" (X "/\" (Y "/\" Z)) by LATTICES:def 7
    .= Z "/\" ((X "/\" Y) "/\" Z) by LATTICES:def 7
    .= Z "/\" Bottom L by A1
    .= Bottom L;
  hence thesis;
end;

begin :: Boolean Lattices

reserve L for B_Lattice;
reserve X,Y,Z,V for Element of L;

theorem
  X \ Y [= Z implies X [= Y "\/" Z
proof
  assume X \ Y [= Z;
  then Y "\/" (X "/\" Y`) [= Y "\/" Z by FILTER_0:1;
  then (Y "\/" X) "/\" (Y "\/" Y`) [= Y "\/" Z by LATTICES:11;
  then
A1: (Y "\/" X) "/\" Top L [= Y "\/" Z by LATTICES:21;
  X [= X "\/" Y by LATTICES:5;
  hence thesis by A1,LATTICES:7;
end;

theorem Th22:
  X [= Y implies Z \ Y [= Z \ X
proof
  assume X [= Y;
  then Y` [= X` by LATTICES:26;
  hence thesis by LATTICES:9;
end;

theorem
  X [= Y & Z [= V implies X \ V [= Y \ Z
proof
  assume X [= Y & Z [= V;
  then X \ V [= Y \ V & Y \ V [= Y \ Z by Th22,LATTICES:9;
  hence thesis by LATTICES:7;
end;

theorem
  X [= Y "\/" Z implies X \ Y [= Z
proof
  assume X [= Y "\/" Z;
  then X "/\" Y` [= (Y "\/" Z) "/\" Y` by LATTICES:9;
  then X "/\" Y` [= (Y "/\" Y`) "\/" (Z "/\" Y`) by LATTICES:def 11;
  then
A1: X \ Y [= Bottom L "\/" (Z "/\" Y`) by LATTICES:20;
  Z "/\" Y` [= Z by LATTICES:6;
  hence thesis by A1,LATTICES:7;
end;

theorem
  X` [= (X "/\" Y)`
proof
  X` [= X` "\/" Y` by LATTICES:5;
  hence thesis by LATTICES:23;
end;

theorem
  (X "\/" Y)` [= X`
proof
  (X "\/" Y)` = X` "/\" Y` by LATTICES:24;
  hence thesis by LATTICES:6;
end;

theorem
  X [= Y \ X implies X = Bottom L
proof
A1: X "/\" (Y "/\" X`) = Y "/\" (X` "/\" X) by LATTICES:def 7
    .= Y "/\" Bottom L by LATTICES:20
    .= Bottom L;
  assume X [= Y \ X;
  hence thesis by A1,LATTICES:4;
end;

theorem
  X [= Y implies Y = X "\/" (Y \ X)
proof
  assume
A1: X [= Y;
  Y = Y "/\" Top L
    .= Y "/\" ( X "\/" X`) by LATTICES:21
    .= (Y "/\" X) "\/" ( Y "/\" X`) by LATTICES:def 11
    .= X "\/" (Y \ X) by A1,LATTICES:4;
  hence thesis;
end;

theorem Th29:
  X \ Y = Bottom L iff X [= Y
proof
  thus X \ Y = Bottom L implies X [= Y
  proof
A1: X "/\" Y` = Bottom L implies X [= Y`` by LATTICES:25;
    assume X \ Y = Bottom L;
    hence thesis by A1;
  end;
  assume X [= Y;
  then X "/\" Y` [= Y` "/\" Y by LATTICES:9;
  then
A2: X "/\" Y` [= Bottom L by LATTICES:20;
  Bottom L [= X \ Y by LATTICES:16;
  hence thesis by A2;
end;

theorem
  X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y
proof
  assume that
A1: X [= (Y "\/" Z) and
A2: X "/\" Z = Bottom L;
  X "/\" (Y "\/" Z) = X by A1,LATTICES:4;
  then (X "/\" Y) "\/" Bottom L = X by A2,LATTICES:def 11;
  hence thesis by LATTICES:4;
end;

theorem
  X "\/" Y = (X \ Y) "\/" Y
proof
  thus X "\/" Y = (X "\/" Y) "/\" Top L
    .= (X "\/" Y) "/\" (Y` "\/" Y) by LATTICES:21
    .= (X \ Y) "\/" Y by LATTICES:11;
end;

theorem
  X \ (X "\/" Y) = Bottom L by Th29,LATTICES:5;

theorem Th33:
  X \ X "/\" Y = X \ Y
proof
  X \ X "/\" Y = X "/\" (X` "\/" Y`) by LATTICES:23
    .= (X "/\" X`) "\/" (X "/\" Y`) by LATTICES:def 11
    .= Bottom L "\/" (X "/\" Y`) by LATTICES:20
    .= X "/\" Y`;
  hence thesis;
end;

theorem
  (X \ Y) "/\" Y = Bottom L
proof
  (X \ Y) "/\" Y = X "/\" (Y`"/\" Y) by LATTICES:def 7
    .= X "/\" Bottom L by LATTICES:20;
  hence thesis;
end;

theorem Th35:
  X "\/" (Y \ X) = X "\/" Y
proof
  X "\/" (Y \ X) = (X "\/" Y) "/\" (X "\/" X`) by LATTICES:11
    .= (X "\/" Y) "/\" Top L by LATTICES:21;
  hence thesis;
end;

theorem Th36:
  (X "/\" Y) "\/" (X \ Y) = X
proof
  (X "/\" Y) "\/" (X \ Y) =((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" Y`)
  by LATTICES:11
    .= X "/\" ((X "/\" Y) "\/" Y`) by LATTICES:def 8
    .= X "/\" ((X "\/" Y`) "/\" (Y "\/" Y`)) by LATTICES:11
    .= X "/\" ((X "\/" Y`) "/\" Top L) by LATTICES:21
    .= X by LATTICES:def 9;
  hence thesis;
end;

theorem Th37:
  X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
proof
  X \ (Y \ Z) = X "/\" (Y`"\/" Z``) by LATTICES:23
    .= X "/\" (Y`"\/" Z)
    .= (X "/\" Y`) "\/" (X "/\" Z) by LATTICES:def 11;
  hence thesis;
end;

theorem
  X \ (X \ Y) = X "/\" Y
proof
  X \ (X \ Y) = X "/\" (X` "\/" Y``) by LATTICES:23
    .= X "/\" (X` "\/" Y)
    .= (X "/\" X`) "\/" (X "/\" Y) by LATTICES:def 11
    .= Bottom L "\/" (X "/\" Y) by LATTICES:20;
  hence thesis;
end;

theorem
  (X "\/" Y) \ Y = X \ Y
proof
  (X "\/" Y) \ Y = (X "/\" Y`) "\/" (Y "/\" Y`) by LATTICES:def 11
    .= (X "/\" Y`) "\/" Bottom L by LATTICES:20
    .= X "/\" Y`;
  hence thesis;
end;

theorem
  X "/\" Y = Bottom L iff X \ Y = X
proof
  thus X "/\" Y = Bottom L implies X \ Y = X
  proof
    assume X "/\" Y = Bottom L;
    then
A1:  X "/\" X [= X "/\" Y` by LATTICES:9,25;
    X \ Y [= X by LATTICES:6;
    hence thesis by A1;
  end;
  assume X \ Y = X;
  then X` "\/" Y`` = X` by LATTICES:23;
  then X "/\" (X` "\/" Y) [= X "/\" X`;
  then (X "/\" X`) "\/" (X "/\" Y) [= X "/\" X` by LATTICES:def 11;
  then Bottom L "\/" (X "/\" Y) [= X "/\" X` by LATTICES:20;
  then
A2: X "/\" Y [= Bottom L by LATTICES:20;
  Bottom L [= X "/\" Y by LATTICES:16;
  hence thesis by A2;
end;

theorem
  X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
proof
  thus X \ (Y "\/" Z) = X "/\" (Y` "/\" Z`) by LATTICES:24
    .= (X "/\" X "/\" Y`) "/\" Z` by LATTICES:def 7
    .= (X "/\" (X "/\" Y`)) "/\" Z` by LATTICES:def 7
    .= (X \ Y) "/\" (X \ Z) by LATTICES:def 7;
end;

theorem Th42:
  X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
proof
  thus X \ (Y "/\" Z) = X "/\" (Y` "\/" Z`) by LATTICES:23
    .= (X \ Y) "\/" (X \ Z) by LATTICES:def 11;
end;

theorem
  X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z
proof
  X "/\" Y \ X "/\" Z = ((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z) by Th42
    .= Bottom L "\/" ((X "/\" Y) \ Z) by Th29,LATTICES:6
    .= (X "/\" Y) \ Z;
  hence thesis by LATTICES:def 7;
end;

theorem Th44:
  (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
proof
  (X "\/" Y) \ (X "/\" Y) = (X "\/" Y) "/\" (X` "\/" Y`) by LATTICES:23
    .= ((X "\/" Y) "/\" X`) "\/" ((X "\/" Y) "/\" Y`) by LATTICES:def 11
    .= ((X "/\" X`) "\/" (Y "/\" X`)) "\/" ((X "\/" Y) "/\" Y`) by
LATTICES:def 11
    .= ((X "/\" X`) "\/" (Y "/\" X`)) "\/" ((X "/\" Y`) "\/" (Y "/\" Y`)) by
LATTICES:def 11
    .= (Bottom L "\/" (Y "/\" X`)) "\/" ((X "/\" Y`) "\/" (Y "/\" Y`)) by
LATTICES:20
    .= (Y "/\" X`) "\/" ((X "/\" Y`) "\/" Bottom L) by LATTICES:20
    .= (X \ Y) "\/" (Y \ X);
  hence thesis;
end;

theorem Th45:
  (X \ Y) \ Z = X \ (Y "\/" Z)
proof
  thus (X \ Y) \ Z = X "/\" (Y` "/\" Z`) by LATTICES:def 7
    .= X \ (Y "\/" Z) by LATTICES:24;
end;

theorem
  X \ Y = Y \ X implies X = Y
proof
  assume
A1: X \ Y = Y \ X;
  then (X "/\" Y`) "/\" X = Y "/\" (X` "/\" X) by LATTICES:def 7
    .= Y "/\" Bottom L by LATTICES:20
    .= Bottom L;
  then (X "/\" X) "/\" Y` = Bottom L by LATTICES:def 7;
  then (X "/\" Y`) "\/" X`= (X "/\" X`) "\/" X` by LATTICES:20
    .= X` by LATTICES:def 8;
  then (X "\/" X`) "/\" (Y` "\/" X`) = X` by LATTICES:11;
  then Top L "/\" (Y` "\/" X`) = X` by LATTICES:21;
  then Y` "/\" X` = Y` by LATTICES:def 9;
  then X`` [= Y`` by LATTICES:4,26;
  then X [= Y``;
  then
A2: X [= Y;
  X "/\" (Y` "/\" Y) = (Y "/\" X`) "/\" Y by A1,LATTICES:def 7;
  then X "/\" Bottom L = (Y "/\" X`) "/\" Y by LATTICES:20;
  then Bottom L
    = X` "/\" (Y "/\" Y) by LATTICES:def 7
    .= X` "/\" Y;
  then Y [= X`` by LATTICES:25;
  then Y [= X;
  hence thesis by A2;
end;

theorem Th47:
  X \ Bottom L = X
proof
  X \ Bottom L = X "/\" Top L by LATTICE4:30
    .= X;
  hence thesis;
end;

theorem
  (X \ Y)` = X` "\/" Y
proof
  (X \ Y)` = X` "\/" Y`` by LATTICES:23;
  hence thesis;
end;

theorem Th49:
  X meets Y "\/" Z iff X meets Y or X meets Z
proof
  thus X meets Y "\/" Z implies X meets Y or X meets Z
  proof
    assume X meets Y "\/" Z;
    then X "/\" (Y "\/" Z) <> Bottom L;
    then (X "/\" Y) "\/" (X "/\" Z) <> Bottom L by LATTICES:def 11;
    then (X "/\" Y) <> Bottom L or (X "/\" Z) <> Bottom L;
    hence thesis;
  end;
  assume
A1: X meets Y or X meets Z;
  per cases by A1;
  suppose
A2: X meets Y;
    X "/\" Y [= (X "/\" Y) "\/" (X "/\" Z) by LATTICES:5;
    then
A3: X "/\" Y [= X "/\" (Y "\/" Z) by LATTICES:def 11;
    X "/\" (Y "\/" Z) <> Bottom L by A3,Th9,A2;
   hence thesis;
  end;
  suppose
A4: X meets Z;
A5: (X "/\" Z) "\/" (X "/\" Y) = X "/\" (Y "\/" Z) by LATTICES:def 11;
    X "/\" Z <> Bottom L by A4;
    then X "/\" (Y "\/" Z) <> Bottom L by A5,Th11;
    hence thesis;
  end;
end;

theorem Th50:
  X "/\" Y misses X \ Y
proof
  (X "/\" Y) "/\" (X \ Y) = (X "/\" Y "/\" Y`) "/\" X by LATTICES:def 7
    .= (X "/\" (Y "/\" Y`)) "/\" X by LATTICES:def 7
    .= Bottom L "/\" X by LATTICES:20
    .= Bottom L;
  hence thesis;
end;

theorem
  X misses Y "\/" Z iff X misses Y & X misses Z by Th49;

theorem
  (X \ Y) misses Y
proof
  (X \ Y) "/\" Y = X "/\" (Y` "/\" Y) by LATTICES:def 7
    .= X "/\" Bottom L by LATTICES:20
    .= Bottom L;
  hence thesis;
end;

theorem
  X misses Y implies (X "\/" Y) \ Y = X
proof
  assume X "/\" Y = Bottom L;
  then X` "\/" (X "/\" Y) = X`;
  then (X` "\/" X) "/\" (X` "\/" Y) = X` by LATTICES:11;
  then Top L "/\" (X` "\/" Y) = X` by LATTICES:21;
  then (X` "\/" Y)` = X;
  then
A1: X`` "/\" Y` = X by LATTICES:24;
  (X "\/" Y) \ Y = (X "/\" Y`) "\/" (Y "/\" Y`) by LATTICES:def 11
    .= (X "/\" Y`) "\/" Bottom L by LATTICES:20
    .= X "/\" Y`;
  hence thesis by A1;
end;

theorem
  X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies X = Y` & Y = X`
proof
  assume that
A1: X` "\/" Y` = X "\/" Y and
A2: X misses X` and
A3: Y misses Y`;
A4: X "/\" X`= Bottom L by A2;
A5: Y "/\" Y` = Bottom L by A3;
  then
A6: Y` "/\" (X` "\/" Y`) = (Y` "/\" X) "\/" Bottom L by A1,LATTICES:def 11;
  (Y "/\" X`) "\/" (Y "/\" Y`) = Y "/\" (X "\/" Y) by A1,LATTICES:def 11;
  then Y "/\" X` = Y "/\" (X "\/" Y) by A5;
  then
A7: Y "/\" X` = Y by LATTICES:def 9;
  (X "/\" X`) "\/" (X "/\" Y`) = X "/\" (X "\/" Y) by A1,LATTICES:def 11;
  then X "/\" Y` = X "/\" (X "\/" Y) by A4
    .= X by LATTICES:def 9;
  hence X = Y` by A6,LATTICES:def 9;
  X` "/\" (X` "\/" Y`) = Bottom L "\/" (X` "/\" Y) by A1,A4,LATTICES:def 11;
  hence thesis by A7,LATTICES:def 9;
end;

theorem
  X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y` implies X = X` & Y = Y`
proof
  assume that
A1: X` "\/" Y` = X "\/" Y and
A2: Y misses X` and
A3: X misses Y`;
A4: Y "/\" X` = Bottom L by A2;
  then (X "\/" Y) "/\" (X "\/" X`) = X "\/" Bottom L by LATTICES:11;
  then (X "\/" Y) "/\" Top L = X by LATTICES:21;
  then (Y "/\" X)` [= Y` by LATTICES:def 9;
  then
A5: X "\/" Y [= Y` by A1,LATTICES:23;
A6: X "/\" Y` = Bottom L by A3;
  then (Y "\/" X) "/\" (Y "\/" Y`) = Y "\/" Bottom L by LATTICES:11;
  then (Y "\/" X) "/\" Top L = Y by LATTICES:21;
  then (X "/\" Y)` [= X` by LATTICES:def 9;
  then
A7: X "\/" Y [= X` by A1,LATTICES:23;
  (Y` "\/" Y) "/\" (Y` "\/" X`) = Y` "\/" Bottom L by A4,LATTICES:11;
  then Top L "/\" (Y` "\/" X`) = Y` by LATTICES:21;
  then (X` "/\" Y`)` [= X`` by LATTICES:def 9;
  then (X` "/\" Y`)` [= X;
  then X`` "\/" Y`` [= X by LATTICES:23;
  then X "\/" Y`` [= X;
  then
A8: X` "\/" Y` [= X by A1;
  X` [= X` "\/" Y` by LATTICES:5;
  then
A9: X` [= X by A8,LATTICES:7;
  (X` "\/" X) "/\" (X` "\/" Y`) = X` "\/" Bottom L by A6,LATTICES:11;
  then Top L "/\" (X` "\/" Y`)= X` by LATTICES:21;
  then (Y` "/\" X`)` [= Y`` by LATTICES:def 9;
  then Y`` "\/" X`` [= Y`` by LATTICES:23;
  then Y`` "\/" X`` [= Y;
  then Y`` "\/" X [= Y;
  then
A10: X` "\/" Y` [= Y by A1;
  Y` [= X` "\/" Y` by LATTICES:5;
  then
A11: Y` [= Y by A10,LATTICES:7;
  X [= X "\/" Y by LATTICES:5;
  then
A12: X [= X` by A7,LATTICES:7;
  Y [= X "\/" Y by LATTICES:5;
  then Y [= Y` by A5,LATTICES:7;
  hence thesis by A11,A9,A12;
end;

theorem
  X \+\ Bottom L = X
by Th47;

theorem
  X \+\ X = Bottom L by LATTICES:20;

theorem
  X "/\" Y misses X \+\ Y
proof
  X "/\" Y misses X \ Y & X "/\" Y misses Y \ X by Th50;
  hence thesis by Th49;
end;

theorem
  X "\/" Y = X \+\ (Y \ X)
proof
  X "\/" Y = (X "\/" Y) "/\" Top L
    .= (X "\/" Y) "/\" (X "\/" X`) by LATTICES:21
    .= X "\/" (Y "/\" X`) by LATTICES:11
    .= ((X "/\" Y`) "\/" (X "/\" X)) "\/" (Y "/\" X`) by LATTICES:def 8
    .= ((X "/\" Y`) "\/" (X "/\" X``)) "\/" (Y "/\" (X` "/\" X`))
    .= (X "/\" (Y` "\/" X``)) "\/" (Y "/\" (X` "/\" X`)) by LATTICES:def 11
    .= (X "/\" (Y "/\" X`)`) "\/" (Y "/\" (X` "/\" X`)) by LATTICES:23
    .= X \+\ (Y \ X) by LATTICES:def 7;
  hence thesis;
end;

theorem
  X \+\ (X "/\" Y) = X \ Y
proof
  X \+\ (X "/\" Y) = (X "/\" (X "/\" Y)`) "\/" (Y "/\" (X "/\" X`)) by
LATTICES:def 7
    .= (X "/\" (X "/\" Y)`) "\/" (Y "/\" Bottom L) by LATTICES:20
    .= X "/\" (X` "\/" Y`) by LATTICES:23
    .= (X "/\" X`) "\/" (X "/\" Y`) by LATTICES:def 11
    .= Bottom L "\/" (X "/\" Y`) by LATTICES:20
    .= X "/\" Y`;
  hence thesis;
end;

theorem
  X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
proof
  thus X "\/" Y = (Y \ X) "\/" X by Th35
    .= (Y \ X) "\/" ((X \ Y) "\/" (X "/\" Y)) by Th36
    .= (X \+\ Y) "\/" (X "/\" Y) by LATTICES:def 5;
end;

Lm1: (X "\/" Y) \ (X \+\ Y) = X "/\" Y
proof
  set XY = X "\/" Y;
  thus XY \ (X \+\ Y) = XY "/\" ((X "/\" Y`)` "/\" (Y "/\" X`)`) by LATTICES:24
    .= XY "/\" ((X "/\" Y`)` "/\" (Y` "\/" X``)) by LATTICES:23
    .= XY "/\" ((X` "\/" Y``) "/\" (Y` "\/" X``)) by LATTICES:23
    .= XY "/\" ((X` "\/" Y``) "/\" (Y` "\/" X))
    .= XY "/\" ((X` "\/" Y) "/\" (Y` "\/" X))
    .= (XY "/\" (X` "\/" Y)) "/\" (Y` "\/" X) by LATTICES:def 7
    .= ( (XY "/\" X`) "\/" ((X "\/" Y) "/\" Y) ) "/\" (Y` "\/" X) by
LATTICES:def 11
    .= ( (XY "/\" X`) "\/" Y ) "/\" (Y` "\/" X) by LATTICES:def 9
    .= ( ((X "/\" X`) "\/" (Y "/\" X`)) "\/" Y ) "/\" (Y` "\/" X) by
LATTICES:def 11
    .= ( (Bottom L "\/" (Y "/\" X`)) "\/" Y ) "/\" (Y` "\/" X) by LATTICES:20
    .= Y "/\" (Y` "\/" X) by LATTICES:def 8
    .= (Y "/\" Y`) "\/" (Y "/\" X) by LATTICES:def 11
    .= Bottom L "\/" (Y "/\" X) by LATTICES:20
    .= X "/\" Y;
end;

theorem
  (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
proof
  set XY = X \+\ Y, A = Y "/\" X`;
  XY \+\ (X "/\" Y) = (XY "/\" (X` "\/" Y`)) "\/" ((X "/\" Y) "/\" XY`) by
LATTICES:23
    .= ( (XY "/\" X`) "\/" (XY "/\" Y`) ) "\/" ((X "/\" Y) "/\" XY`) by
LATTICES:def 11
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X "/\" Y`)` "/\" A
  `) ) by LATTICES:24
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y``) "/\"
  A`) ) by LATTICES:23
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y``) "/\"
  (Y` "\/" X``)) ) by LATTICES:23
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y) "/\" (Y
  ` "\/" X``)) )
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Y) "/\" ((X` "\/" Y) "/\" (Y
  ` "\/" X)) )
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (((X "/\" Y) "/\" (X` "\/" Y)) "/\" (
  Y` "\/" X)) by LATTICES:def 7
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( (((X "/\" Y) "/\" X`) "\/" ((X "/\"
  Y) "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:def 11
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( ((Y "/\" (X "/\" X`)) "\/" ((X "/\"
  Y) "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:def 7
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ( ((Y "/\" Bottom L) "\/" ((X "/\" Y)
  "/\" Y)) "/\" (Y` "\/" X)) by LATTICES:20
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" (Y "/\" Y)) "/\" (Y` "\/" X)
  ) by LATTICES:def 7
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (((X "/\" Y) "/\" Y`) "\/" ((X "/\" Y
  ) "/\" X)) by LATTICES:def 11
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" (Y "/\" Y`)) "\/" ((X "/\" Y
  ) "/\" X)) by LATTICES:def 7
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" ((X "/\" Bottom L) "\/" ((X "/\" Y)
  "/\" X)) by LATTICES:20
    .= ( (XY \ X) "\/" (XY \ Y) ) "\/" (Y "/\" (X "/\" X)) by LATTICES:def 7
    .= ( (((X "/\" Y`) "/\" X`) "\/" (A "/\" X`)) "\/" (((X \ Y) "\/" (Y \ X
  )) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 11
    .= ( ((Y` "/\" (X "/\" X`)) "\/" (A "/\" X`)) "\/" (((X \ Y) "\/" (Y \ X
  )) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 7
    .= ( ((Y` "/\" (X "/\" X`)) "\/" (Y "/\" (X` "/\" X`))) "\/" (((X \ Y)
  "\/" (Y \ X)) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:def 7
    .= ( ((Y` "/\" Bottom L) "\/" (Y "/\" (X` "/\" X`))) "\/" (((X \ Y) "\/"
  (Y \ X)) "/\" Y`) ) "\/" (Y "/\" X) by LATTICES:20
    .= ( A "\/" (((X "/\" Y`) "/\" Y`) "\/" (A "/\" Y`)) ) "\/" (Y "/\" X)
  by LATTICES:def 11
    .= ( A "\/" ( (X "/\" (Y` "/\" Y`)) "\/" (A "/\" Y`)) ) "\/" (Y "/\" X)
  by LATTICES:def 7
    .= ( A "\/" ( (X "/\" Y`) "\/" (X` "/\" (Y "/\" Y`))) ) "\/" (Y "/\" X)
  by LATTICES:def 7
    .= ( A "\/" ((X "/\" Y`) "\/" (X` "/\" Bottom L) )) "\/" (Y "/\" X) by
LATTICES:20
    .= A "\/" ( (X "/\" Y`) "\/" (Y "/\" X) ) by LATTICES:def 5
    .= A "\/" (X "/\" (Y` "\/" Y) ) by LATTICES:def 11
    .= A "\/" (X "/\" Top L) by LATTICES:21
    .= (Y "\/" X) "/\" (X` "\/" X ) by LATTICES:11
    .= (Y "\/" X) "/\" Top L by LATTICES:21
    .= Y "\/" X;
  hence thesis;
end;

theorem
  (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
proof
  (X \+\ Y) \+\ (X "\/" Y) = ((X \+\ Y) "/\" (X` "/\" Y`)) "\/" ((X "\/" Y
  ) \ (X \+\ Y)) by LATTICES:24
    .= ( ((X "/\" Y`) "/\" (X` "/\" Y`)) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)
  ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 11
    .= ( (X "/\" (Y` "/\" (Y` "/\" X`))) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)
  ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
    .= ( (X "/\" ((Y` "/\" Y`) "/\" X`)) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)
  ) ) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
    .= ( ((X "/\" X`) "/\" Y`) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)) ) "\/" (
  (X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
    .= ( (Bottom L "/\" Y`) "\/" ((Y "/\" X`) "/\" (X` "/\" Y`)) ) "\/" ((X
  "\/" Y) \ (X \+\ Y)) by LATTICES:20
    .= (Y "/\" (X` "/\" (X` "/\" Y`))) "\/" ((X "\/" Y) \ (X \+\ Y)) by
LATTICES:def 7
    .= (Y "/\" ((X` "/\" X`) "/\" Y`)) "\/" ((X "\/" Y) \ (X \+\ Y)) by
LATTICES:def 7
    .= ((Y "/\" Y`) "/\" X`) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
    .= (Bottom L "/\" X`) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:20
    .= Y "/\" X by Lm1;
  hence thesis;
end;

theorem Th64:
  X \+\ Y = (X "\/" Y) \ (X "/\" Y)
proof
  thus X \+\ Y = (X \ X "/\" Y) "\/" (Y \ X) by Th33
    .= (X \ X "/\" Y) "\/" (Y \ X "/\" Y) by Th33
    .= (X "\/" Y) \ (X "/\" Y) by LATTICES:def 11;
end;

theorem
  (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
proof
  thus (X \+\ Y) \ Z = (X \ Y \ Z) "\/" (Y \ X \ Z) by LATTICES:def 11
    .= (X \ (Y "\/" Z)) "\/" (Y \ X \ Z) by Th45
    .= (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z)) by Th45;
end;

theorem
  X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z)
proof
  X \ (Y \+\ Z) = X \ ((Y "\/" Z) \ (Y "/\" Z)) by Th64
    .= (X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z)) by Th37
    .= (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z) by LATTICES:def 7;
  hence thesis;
end;

theorem
  (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
  set S1 = X \ (Y "\/" Z), S2 = Y \ (X "\/" Z), S3 = Z \ (X "\/" Y), S4 = X
  "/\" Y "/\" Z;
  thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y)
  "\/" (Y \ X))) by LATTICES:def 11
    .= ( S1 "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
    .= ( S1 "\/" S2) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
    .= ( S1 "\/" S2) "\/" (Z \ ((X "\/" Y) \ (X "/\" Y))) by Th44
    .= ( S1 "\/" S2) "\/" (S3 "\/" (X "/\" Y "/\" Z )) by Th37
    .= (S1 "\/" S2 "\/" S4) "\/" S3 by LATTICES:def 5
    .= (S1 "\/" S4 "\/" S2) "\/" S3 by LATTICES:def 5
    .= (S1 "\/" S4) "\/" (S2 "\/" S3) by LATTICES:def 5
    .= (S1 "\/" (X "/\" (Y "/\" Z))) "\/" (S2 "\/" S3) by LATTICES:def 7
    .= (X \ ((Y "\/" Z) \ (Y "/\" Z))) "\/" (S2 "\/" S3) by Th37
    .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" S3) by Th44
    .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (S2 "\/" (Z \ Y \ X)) by Th45
    .= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ Z \ X) "\/" (Z \ Y \ X)) by Th45
    .= X \+\ (Y \+\ Z) by LATTICES:def 11;
end;

theorem
  (X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`)
proof
  thus (X \+\ Y)` = (X \ Y)` "/\" (Y \ X)` by LATTICES:24
    .=(X` "\/" Y``) "/\" (Y "/\" X`)` by LATTICES:23
    .=(X` "\/" Y``) "/\" (Y` "\/" X``) by LATTICES:23
    .=(X` "\/" Y) "/\" (Y` "\/" X``)
    .=(X` "\/" Y) "/\" (Y` "\/" X)
    .=(X` "/\" (Y` "\/" X)) "\/" (Y "/\" (Y` "\/" X)) by LATTICES:def 11
    .=((X` "/\" Y`) "\/" (X` "/\" X)) "\/" (Y "/\" (Y` "\/" X)) by
LATTICES:def 11
    .=((X` "/\" Y`) "\/" (X` "/\" X)) "\/" ((Y "/\" Y`) "\/" (Y "/\" X)) by
LATTICES:def 11
    .=((X` "/\" Y`) "\/" Bottom L) "\/" ((Y "/\" Y`) "\/" (Y "/\" X)) by
LATTICES:20
    .=(X` "/\" Y`) "\/" (Bottom L "\/" (Y "/\" X)) by LATTICES:20
    .=(X "/\" Y) "\/" (X` "/\" Y`);
end;