:: BOOLEALG semantic presentation

begin


definition
let L be Lattice;
let X, Y be Element of L;
funcX \ Y ->  Element of L equals :: BOOLEALG:def 1
X "/\" (Y `);
coherence
 X "/\" (Y `) is Element of L ;
end;

:: deftheorem  defines \ BOOLEALG:def_1_:_
 for L being Lattice
for X, Y being Element of L holds X \ Y = X "/\" (Y `);

definition
let L be Lattice;
let X, Y be Element of L;
funcX \+\ Y ->  Element of L equals :: BOOLEALG:def 2
(X \ Y) "\/" (Y \ X);
coherence
 (X \ Y) "\/" (Y \ X) is Element of L ;
end;

:: deftheorem  defines \+\ BOOLEALG:def_2_:_
 for L being Lattice
for X, Y being Element of L holds X \+\ Y = (X \ Y) "\/" (Y \ X);

definition
let L be Lattice;
let X, Y be Element of L;
:: original: =
redefine predX = Y means :Def3: :: BOOLEALG:def 3
( X [= Y & Y [= X );
compatibility
 ( X = Y iff ( X [= Y & Y [= X ) ) by LATTICES:8;
end;

:: deftheorem Def3 defines = BOOLEALG:def_3_:_
 for L being Lattice
for X, Y being Element of L holds
( X = Y iff ( X [= Y & Y [= X ) );

definition
let L be Lattice;
let X, Y be Element of L;
predX meets Y means :Def4: :: BOOLEALG:def 4
X "/\" Y <> Bottom L;
end;

:: deftheorem Def4 defines meets BOOLEALG:def_4_:_
 for L being Lattice
for X, Y being Element of L holds
( X meets Y iff X "/\" Y <> Bottom L );

notation
let L be Lattice;
let X, Y be Element of L;
antonym X misses Y for X meets Y;
end;

theorem :: BOOLEALG:1
for L being Lattice
for X, Y, Z being Element of L st X "\/" Y [= Z holds
X [= Z
proof
let L be Lattice; ::_thesis: for X, Y, Z being Element of L st X "\/" Y [= Z holds
X [= Z
let X, Y, Z be Element of L; ::_thesis: ( X "\/" Y [= Z implies X [= Z )
assume  X "\/" Y [= Z ; ::_thesis: X [= 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  X [= Z by A1, LATTICES:7; ::_thesis: verum
end;

theorem :: BOOLEALG:2
for L being Lattice
for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z
proof
let L be Lattice; ::_thesis: for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z
let X, Y, Z be Element of L; ::_thesis: X "/\" Y [= X "\/" Z
 ( X "/\" Y [= X & X [= X "\/" Z ) by LATTICES:5, LATTICES:6;
hence  X "/\" Y [= X "\/" Z by LATTICES:7; ::_thesis: verum
end;

theorem :: BOOLEALG:3
for L being Lattice
for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z
proof
let L be Lattice; ::_thesis: for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z
let X, Z, Y be Element of L; ::_thesis: ( X [= Z implies X \ Y [= Z )
assume  X [= Z ; ::_thesis: X \ Y [= Z
then A1: X "/\" (Y `) [= Z "/\" (Y `) by LATTICES:9;
 Z "/\" (Y `) [= Z by LATTICES:6;
hence  X \ Y [= Z by A1, LATTICES:7; ::_thesis: verum
end;

theorem :: BOOLEALG:4
for L being Lattice
for X, Y, Z being Element of L st X \ Y [= Z & Y \ X [= Z holds
X \+\ Y [= Z by FILTER_0:6;

theorem :: BOOLEALG:5
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "\/" Z iff ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) )
proof
let L be Lattice; ::_thesis: for X, Y, Z being Element of L holds
( X = Y "\/" Z iff ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) )
let X, Y, Z be Element of L; ::_thesis: ( X = Y "\/" Z iff ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) )
thus  ( X = Y "\/" Z implies ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) ) by FILTER_0:6, LATTICES:5; ::_thesis: ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) implies X = Y "\/" Z )
assume that
A1: ( Y [= X & Z [= X ) and
A2: for V being Element of L st Y [= V & Z [= V holds
X [= V ; ::_thesis: X = Y "\/" Z
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  X = Y "\/" Z by A3, LATTICES:8; ::_thesis: verum
end;

theorem :: BOOLEALG:6
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
proof
let L be Lattice; ::_thesis: for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
let X, Y, Z be Element of L; ::_thesis: ( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
thus  ( X = Y "/\" Z implies ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) ) by FILTER_0:7, LATTICES:6; ::_thesis: ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) implies X = Y "/\" Z )
assume that
A1: ( X [= Y & X [= Z ) and
A2: for V being Element of L st V [= Y & V [= Z holds
V [= X ; ::_thesis: X = Y "/\" Z
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  X = Y "/\" Z by A3, Def3; ::_thesis: verum
end;

Lm1:  for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X
proof
let L be Lattice; ::_thesis: for X, Y being Element of L st X meets Y holds
Y meets X
let X, Y be Element of L; ::_thesis: ( X meets Y implies Y meets X )
assume  X meets Y ; ::_thesis: Y meets X
then  X "/\" Y <> Bottom L by Def4;
hence  Y meets X by Def4; ::_thesis: verum
end;

theorem :: BOOLEALG:7
for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L )
proof
let L be Lattice; ::_thesis: for X being Element of L holds
( X meets X iff X <> Bottom L )
let X be Element of L; ::_thesis: ( X meets X iff X <> Bottom L )
A1: X "/\" X = X ;
hereby  ::_thesis: ( X <> Bottom L implies X meets X )
assume  X meets X ; ::_thesis: X <> Bottom L
then  X "/\" X <> Bottom L by Def4;
hence  X <> Bottom L ; ::_thesis: verum
end;
assume  X <> Bottom L ; ::_thesis: X meets X
hence  X meets X by A1, Def4; ::_thesis: verum
end;

definition
let L be Lattice;
let X, Y be Element of L;
:: original: meets
redefine predX meets Y;
symmetry
 for X, Y being Element of L st (L,b1,b2) holds
(L,b2,b1) by Lm1;
:: original: \+\
redefine funcX \+\ Y ->  Element of L;
commutativity
 for X, Y being Element of L holds X \+\ Y = Y \+\ X ;
:: original: meets
redefine predX misses Y;
symmetry
 for X, Y being Element of L st (L,b1,b2) holds
not (L,b2,b1) by Lm1;
end;

begin

begin


theorem :: BOOLEALG:8
for L being D_Lattice
for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z
proof
let L be D_Lattice; ::_thesis: for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z
let X, Y, Z be Element of L; ::_thesis: ( (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z )
assume  (X "/\" Y) "\/" (X "/\" Z) = X ; ::_thesis: X [= Y "\/" Z
then  X "/\" (Y "\/" Z) = X by LATTICES:def_11;
hence  X [= Y "\/" Z by LATTICES:4; ::_thesis: verum
end;

begin


theorem Th9: :: BOOLEALG:9
for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L
proof
let L be 0_Lattice; ::_thesis: for X being Element of L st X [= Bottom L holds
X = Bottom L
let X be Element of L; ::_thesis: ( X [= Bottom L implies X = Bottom L )
A1: Bottom L [= X by LATTICES:16;
assume  X [= Bottom L ; ::_thesis: X = Bottom L
hence  X = Bottom L by A1, LATTICES:8; ::_thesis: verum
end;

theorem :: BOOLEALG:10
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y "/\" Z = Bottom L holds
X = Bottom L by Th9, FILTER_0:7;

theorem Th11: :: BOOLEALG:11
for L being 0_Lattice
for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
proof
let L be 0_Lattice; ::_thesis: for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
let X, Y be Element of L; ::_thesis: ( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
thus  ( X "\/" Y = Bottom L implies ( X = Bottom L & Y = Bottom L ) ) ::_thesis: ( X = Bottom L & Y = Bottom L implies X "\/" Y = Bottom L )
proof
assume  X "\/" Y = Bottom L ; ::_thesis: ( X = Bottom L & Y = Bottom L )
then A1: ( X [= Bottom L & Y [= Bottom L ) by LATTICES:5;
 ( Bottom L [= X & Bottom L [= Y ) by LATTICES:16;
hence  ( X = Bottom L & Y = Bottom L ) by A1, Def3; ::_thesis: verum
end;
thus  ( X = Bottom L & Y = Bottom L implies X "\/" Y = Bottom L ) by LATTICES:14; ::_thesis: verum
end;

theorem :: BOOLEALG:12
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & Y "/\" Z = Bottom L holds
X "/\" Z = Bottom L by LATTICES:9, Th9;

theorem Th13: :: BOOLEALG:13
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z
proof
let L be 0_Lattice; ::_thesis: for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z
let X, Y, Z be Element of L; ::_thesis: ( X meets Y & Y [= Z implies X meets Z )
assume that
A1: X meets Y and
A2: Y [= Z ; ::_thesis: X meets Z
 X "/\" Y <> Bottom L by A1, Def4;
then  X "/\" Z <> Bottom L by A2, Th9, LATTICES:9;
hence  X meets Z by Def4; ::_thesis: verum
end;

theorem Th14: :: BOOLEALG:14
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y & X meets Z )
proof
let L be 0_Lattice; ::_thesis: for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y & X meets Z )
let X, Y, Z be Element of L; ::_thesis: ( X meets Y "/\" Z implies ( X meets Y & X meets Z ) )
assume  X meets Y "/\" Z ; ::_thesis: ( X meets Y & X meets Z )
then A1: X "/\" (Y "/\" Z) <> Bottom L by Def4;
then  (X "/\" Z) "/\" Y <> Bottom L by LATTICES:def_7;
then A2: X "/\" Z <> Bottom L by LATTICES:15;
 (X "/\" Y) "/\" Z <> Bottom L by A1, LATTICES:def_7;
then  X "/\" Y <> Bottom L by LATTICES:15;
hence  ( X meets Y & X meets Z ) by A2, Def4; ::_thesis: verum
end;

theorem :: BOOLEALG:15
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y
proof
let L be 0_Lattice; ::_thesis: for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y
let X, Y, Z be Element of L; ::_thesis: ( X meets Y \ Z implies X meets Y )
assume  X meets Y \ Z ; ::_thesis: X meets Y
then  X "/\" (Y \ Z) <> Bottom L by Def4;
then  (X "/\" Y) "/\" (Z `) <> Bottom L by LATTICES:def_7;
then  X "/\" Y <> Bottom L by LATTICES:15;
hence  X meets Y by Def4; ::_thesis: verum
end;

theorem :: BOOLEALG:16
for L being 0_Lattice
for X being Element of L holds X misses Bottom L
proof
let L be 0_Lattice; ::_thesis: for X being Element of L holds X misses Bottom L
let X be Element of L; ::_thesis: X misses Bottom L
assume  X meets Bottom L ; ::_thesis: contradiction
then  X "/\" (Bottom L) <> Bottom L by Def4;
hence  contradiction ; ::_thesis: verum
end;

theorem :: BOOLEALG:17
for L being 0_Lattice
for X, Z, Y being Element of L st X misses Z & Y [= Z holds
X misses Y by Th13;

theorem :: BOOLEALG:18
for L being 0_Lattice
for X, Y, Z being Element of L st ( X misses Y or X misses Z ) holds
X misses Y "/\" Z by Th14;

theorem :: BOOLEALG:19
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L
proof
let L be 0_Lattice; ::_thesis: for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L
let X, Y, Z be Element of L; ::_thesis: ( X [= Y & X [= Z & Y misses Z implies X = Bottom L )
assume that
A1: ( X [= Y & X [= Z ) and
A2: Y misses Z ; ::_thesis: X = Bottom L
 Y "/\" Z = Bottom L by A2, Def4;
hence  X = Bottom L by A1, Th9, FILTER_0:7; ::_thesis: verum
end;

theorem :: BOOLEALG:20
for L being 0_Lattice
for X, Y, Z being Element of L st X misses Y holds
Z "/\" X misses Z "/\" Y
proof
let L be 0_Lattice; ::_thesis: for X, Y, Z being Element of L st X misses Y holds
Z "/\" X misses Z "/\" Y
let X, Y, Z be Element of L; ::_thesis: ( X misses Y implies Z "/\" X misses Z "/\" Y )
assume A1: X misses Y ; ::_thesis: Z "/\" X misses Z "/\" 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, Def4
.= Bottom L ;
hence  Z "/\" X misses Z "/\" Y by Def4; ::_thesis: verum
end;

begin


theorem :: BOOLEALG:21
for L being B_Lattice
for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z
let X, Y, Z be Element of L; ::_thesis: ( X \ Y [= Z implies X [= Y "\/" Z )
assume  X \ Y [= Z ; ::_thesis: X [= Y "\/" Z
then  Y "\/" (X "/\" (Y `)) [= Y "\/" Z by FILTER_0:1;
then  (Y "\/" X) "/\" (Y "\/" (Y `)) [= Y "\/" Z by LATTICES:11;
then B1: (Y "\/" X) "/\" (Top L) [= Y "\/" Z by LATTICES:21;
 X [= X "\/" Y by LATTICES:5;
hence  X [= Y "\/" Z by B1, LATTICES:7; ::_thesis: verum
end;

theorem Th22: :: BOOLEALG:22
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X
let X, Y, Z be Element of L; ::_thesis: ( X [= Y implies Z \ Y [= Z \ X )
assume  X [= Y ; ::_thesis: Z \ Y [= Z \ X
then  Y ` [= X ` by LATTICES:26;
hence  Z \ Y [= Z \ X by LATTICES:9; ::_thesis: verum
end;

theorem :: BOOLEALG:23
for L being B_Lattice
for X, Y, Z, V being Element of L st X [= Y & Z [= V holds
X \ V [= Y \ Z
proof
let L be B_Lattice; ::_thesis: for X, Y, Z, V being Element of L st X [= Y & Z [= V holds
X \ V [= Y \ Z
let X, Y, Z, V be Element of L; ::_thesis: ( X [= Y & Z [= V implies X \ V [= Y \ Z )
assume  ( X [= Y & Z [= V ) ; ::_thesis: X \ V [= Y \ Z
then  ( X \ V [= Y \ V & Y \ V [= Y \ Z ) by Th22, LATTICES:9;
hence  X \ V [= Y \ Z by LATTICES:7; ::_thesis: verum
end;

theorem :: BOOLEALG:24
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z holds
X \ Y [= Z
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L st X [= Y "\/" Z holds
X \ Y [= Z
let X, Y, Z be Element of L; ::_thesis: ( X [= Y "\/" Z implies X \ Y [= Z )
assume  X [= Y "\/" Z ; ::_thesis: X \ Y [= Z
then  X "/\" (Y `) [= (Y "\/" Z) "/\" (Y `) by LATTICES:9;
then  X "/\" (Y `) [= (Y "/\" (Y `)) "\/" (Z "/\" (Y `)) by LATTICES:def_11;
then B1: X \ Y [= (Bottom L) "\/" (Z "/\" (Y `)) by LATTICES:20;
 Z "/\" (Y `) [= Z by LATTICES:6;
hence  X \ Y [= Z by B1, LATTICES:7; ::_thesis: verum
end;

theorem :: BOOLEALG:25
for L being B_Lattice
for X, Y being Element of L holds X ` [= (X "/\" Y) `
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X ` [= (X "/\" Y) `
let X, Y be Element of L; ::_thesis: X ` [= (X "/\" Y) `
 X ` [= (X `) "\/" (Y `) by LATTICES:5;
hence  X ` [= (X "/\" Y) ` by LATTICES:23; ::_thesis: verum
end;

theorem :: BOOLEALG:26
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) ` [= X `
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X "\/" Y) ` [= X `
let X, Y be Element of L; ::_thesis: (X "\/" Y) ` [= X `
 (X "\/" Y) ` = (X `) "/\" (Y `) by LATTICES:24;
hence  (X "\/" Y) ` [= X ` by LATTICES:6; ::_thesis: verum
end;

theorem :: BOOLEALG:27
for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st X [= Y \ X holds
X = Bottom L
let X, Y be Element of L; ::_thesis: ( X [= Y \ X implies X = Bottom L )
A1: X "/\" (Y "/\" (X `)) = Y "/\" ((X `) "/\" X) by LATTICES:def_7
.= Y "/\" (Bottom L) by LATTICES:20
.= Bottom L ;
assume  X [= Y \ X ; ::_thesis: X = Bottom L
hence  X = Bottom L by A1, LATTICES:4; ::_thesis: verum
end;

theorem :: BOOLEALG:28
for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)
let X, Y be Element of L; ::_thesis: ( X [= Y implies Y = X "\/" (Y \ X) )
assume A1: X [= Y ; ::_thesis: Y = X "\/" (Y \ X)
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  Y = X "\/" (Y \ X) ; ::_thesis: verum
end;

theorem Th29: :: BOOLEALG:29
for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )
let X, Y be Element of L; ::_thesis: ( X \ Y = Bottom L iff X [= Y )
thus  ( X \ Y = Bottom L implies X [= Y ) ::_thesis: ( X [= Y implies X \ Y = Bottom L )
proof
A1: ( X "/\" (Y `) = Bottom L implies X [= (Y `) ` ) by LATTICES:25;
assume  X \ Y = Bottom L ; ::_thesis: X [= Y
hence  X [= Y by A1; ::_thesis: verum
end;
assume  X [= Y ; ::_thesis: X \ Y = Bottom L
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  X \ Y = Bottom L by A2, Def3; ::_thesis: verum
end;

theorem :: BOOLEALG:30
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z & X "/\" Z = Bottom L holds
X [= Y
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L st X [= Y "\/" Z & X "/\" Z = Bottom L holds
X [= Y
let X, Y, Z be Element of L; ::_thesis: ( X [= Y "\/" Z & X "/\" Z = Bottom L implies X [= Y )
assume that
A1: X [= Y "\/" Z and
A2: X "/\" Z = Bottom L ; ::_thesis: X [= Y
 X "/\" (Y "\/" Z) = X by A1, LATTICES:4;
then  (X "/\" Y) "\/" (Bottom L) = X by A2, LATTICES:def_11;
hence  X [= Y by LATTICES:4; ::_thesis: verum
end;

theorem :: BOOLEALG:31
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y
let X, Y be Element of L; ::_thesis: X "\/" Y = (X \ Y) "\/" Y
thus X "\/" Y = (X "\/" Y) "/\" (Top L)
.= (X "\/" Y) "/\" ((Y `) "\/" Y) by LATTICES:21
.= (X \ Y) "\/" Y by LATTICES:11 ; ::_thesis: verum
end;

theorem :: BOOLEALG:32
for L being B_Lattice
for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L by Th29, LATTICES:5;

theorem Th33: :: BOOLEALG:33
for L being B_Lattice
for X, Y being Element of L holds X \ (X "/\" Y) = X \ Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X \ (X "/\" Y) = X \ Y
let X, Y be Element of L; ::_thesis: X \ (X "/\" Y) = X \ Y
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  X \ (X "/\" Y) = X \ Y ; ::_thesis: verum
end;

theorem :: BOOLEALG:34
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L
let X, Y be Element of L; ::_thesis: (X \ Y) "/\" Y = Bottom L
(X \ Y) "/\" Y = X "/\" ((Y `) "/\" Y) by LATTICES:def_7
.= X "/\" (Bottom L) by LATTICES:20 ;
hence  (X \ Y) "/\" Y = Bottom L ; ::_thesis: verum
end;

theorem Th35: :: BOOLEALG:35
for L being B_Lattice
for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y
let X, Y be Element of L; ::_thesis: X "\/" (Y \ X) = X "\/" Y
X "\/" (Y \ X) = (X "\/" Y) "/\" (X "\/" (X `)) by LATTICES:11
.= (X "\/" Y) "/\" (Top L) by LATTICES:21 ;
hence  X "\/" (Y \ X) = X "\/" Y ; ::_thesis: verum
end;

theorem Th36: :: BOOLEALG:36
for L being B_Lattice
for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X
let X, Y be Element of L; ::_thesis: (X "/\" Y) "\/" (X \ Y) = X
(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  (X "/\" Y) "\/" (X \ Y) = X ; ::_thesis: verum
end;

theorem Th37: :: BOOLEALG:37
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
let X, Y, Z be Element of L; ::_thesis: X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
X \ (Y \ Z) = X "/\" ((Y `) "\/" ((Z `) `)) by LATTICES:23
.= X "/\" ((Y `) "\/" Z)
.= (X "/\" (Y `)) "\/" (X "/\" Z) by LATTICES:def_11 ;
hence  X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z) ; ::_thesis: verum
end;

theorem :: BOOLEALG:38
for L being B_Lattice
for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y
let X, Y be Element of L; ::_thesis: X \ (X \ Y) = X "/\" Y
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  X \ (X \ Y) = X "/\" Y ; ::_thesis: verum
end;

theorem :: BOOLEALG:39
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y
let X, Y be Element of L; ::_thesis: (X "\/" Y) \ Y = X \ Y
(X "\/" Y) \ Y = (X "/\" (Y `)) "\/" (Y "/\" (Y `)) by LATTICES:def_11
.= (X "/\" (Y `)) "\/" (Bottom L) by LATTICES:20
.= X "/\" (Y `) ;
hence  (X "\/" Y) \ Y = X \ Y ; ::_thesis: verum
end;

theorem :: BOOLEALG:40
for L being B_Lattice
for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )
let X, Y be Element of L; ::_thesis: ( X "/\" Y = Bottom L iff X \ Y = X )
thus  ( X "/\" Y = Bottom L implies X \ Y = X ) ::_thesis: ( X \ Y = X implies X "/\" Y = Bottom L )
proof
assume  X "/\" Y = Bottom L ; ::_thesis: X \ Y = X
then B1: X "/\" X [= X "/\" (Y `) by LATTICES:9, LATTICES:25;
 X \ Y [= X by LATTICES:6;
hence  X \ Y = X by B1, Def3; ::_thesis: verum
end;
assume  X \ Y = X ; ::_thesis: X "/\" Y = Bottom L
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  X "/\" Y = Bottom L by A2, Def3; ::_thesis: verum
end;

theorem :: BOOLEALG:41
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
let X, Y, Z be Element of L; ::_thesis: X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
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 ; ::_thesis: verum
end;

theorem Th42: :: BOOLEALG:42
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
let X, Y, Z be Element of L; ::_thesis: X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
thus X \ (Y "/\" Z) = X "/\" ((Y `) "\/" (Z `)) by LATTICES:23
.= (X \ Y) "\/" (X \ Z) by LATTICES:def_11 ; ::_thesis: verum
end;

theorem :: BOOLEALG:43
for L being B_Lattice
for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)
let X, Y, Z be Element of L; ::_thesis: X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)
(X "/\" Y) \ (X "/\" Z) = ((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z) by Th42
.= (Bottom L) "\/" ((X "/\" Y) \ Z) by LATTICES:6, Th29
.= (X "/\" Y) \ Z ;
hence  X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z) by LATTICES:def_7; ::_thesis: verum
end;

theorem Th44: :: BOOLEALG:44
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
let X, Y be Element of L; ::_thesis: (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
(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  (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X) ; ::_thesis: verum
end;

theorem Th45: :: BOOLEALG:45
for L being B_Lattice
for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)
let X, Y, Z be Element of L; ::_thesis: (X \ Y) \ Z = X \ (Y "\/" Z)
thus (X \ Y) \ Z = X "/\" ((Y `) "/\" (Z `)) by LATTICES:def_7
.= X \ (Y "\/" Z) by LATTICES:24 ; ::_thesis: verum
end;

theorem :: BOOLEALG:46
for L being B_Lattice
for X, Y being Element of L st X \ Y = Y \ X holds
X = Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st X \ Y = Y \ X holds
X = Y
let X, Y be Element of L; ::_thesis: ( X \ Y = Y \ X implies X = Y )
assume A1: X \ Y = Y \ X ; ::_thesis: X = Y
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, LATTICES: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  X = Y by A2, Def3; ::_thesis: verum
end;

theorem Th47: :: BOOLEALG:47
for L being B_Lattice
for X being Element of L holds X \ (Bottom L) = X
proof
let L be B_Lattice; ::_thesis: for X being Element of L holds X \ (Bottom L) = X
let X be Element of L; ::_thesis: X \ (Bottom L) = X
X \ (Bottom L) = X "/\" (Top L) by LATTICE4:30
.= X ;
hence  X \ (Bottom L) = X ; ::_thesis: verum
end;

theorem :: BOOLEALG:48
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) ` = (X `) "\/" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X \ Y) ` = (X `) "\/" Y
let X, Y be Element of L; ::_thesis: (X \ Y) ` = (X `) "\/" Y
 (X \ Y) ` = (X `) "\/" ((Y `) `) by LATTICES:23;
hence  (X \ Y) ` = (X `) "\/" Y ; ::_thesis: verum
end;

theorem Th49: :: BOOLEALG:49
for L being B_Lattice
for X, Y, Z being Element of L holds
( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds
( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )
let X, Y, Z be Element of L; ::_thesis: ( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )
thus  ( not X meets Y "\/" Z or X meets Y or X meets Z ) ::_thesis: ( ( X meets Y or X meets Z ) implies X meets Y "\/" Z )
proof
assume  X meets Y "\/" Z ; ::_thesis: ( X meets Y or X meets Z )
then  X "/\" (Y "\/" Z) <> Bottom L by Def4;
then  (X "/\" Y) "\/" (X "/\" Z) <> Bottom L by LATTICES:def_11;
then  ( X "/\" Y <> Bottom L or X "/\" Z <> Bottom L ) by LATTICES:14;
hence  ( X meets Y or X meets Z ) by Def4; ::_thesis: verum
end;
assume A1: ( X meets Y or X meets Z ) ; ::_thesis: X meets Y "\/" Z
percases ( X meets Y or X meets Z ) by A1;
supposeA2: X meets Y ; ::_thesis: X meets Y "\/" Z
 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, Def4;
hence  X meets Y "\/" Z by Def4; ::_thesis: verum
end;
supposeA4: X meets Z ; ::_thesis: X meets Y "\/" Z
A5: (X "/\" Z) "\/" (X "/\" Y) = X "/\" (Y "\/" Z) by LATTICES:def_11;
 X "/\" Z <> Bottom L by A4, Def4;
then  X "/\" (Y "\/" Z) <> Bottom L by A5, Th11;
hence  X meets Y "\/" Z by Def4; ::_thesis: verum
end;
end;
end;

theorem Th50: :: BOOLEALG:50
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \ Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "/\" Y misses X \ Y
let X, Y be Element of L; ::_thesis: X "/\" Y misses X \ Y
(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  X "/\" Y misses X \ Y by Def4; ::_thesis: verum
end;

theorem :: BOOLEALG:51
for L being B_Lattice
for X, Y, Z being Element of L holds
( X misses Y "\/" Z iff ( X misses Y & X misses Z ) ) by Th49;

theorem :: BOOLEALG:52
for L being B_Lattice
for X, Y being Element of L holds X \ Y misses Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X \ Y misses Y
let X, Y be Element of L; ::_thesis: X \ Y misses Y
(X \ Y) "/\" Y = X "/\" ((Y `) "/\" Y) by LATTICES:def_7
.= X "/\" (Bottom L) by LATTICES:20
.= Bottom L ;
hence  X \ Y misses Y by Def4; ::_thesis: verum
end;

theorem :: BOOLEALG:53
for L being B_Lattice
for X, Y being Element of L st X misses Y holds
(X "\/" Y) \ Y = X
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st X misses Y holds
(X "\/" Y) \ Y = X
let X, Y be Element of L; ::_thesis: ( X misses Y implies (X "\/" Y) \ Y = X )
assume  X "/\" Y = Bottom L ; :: according to BOOLEALG:def_4 ::_thesis: (X "\/" Y) \ Y = X
then  (X `) "\/" (X "/\" Y) = X ` by LATTICES:14;
then  ((X `) "\/" X) "/\" ((X `) "\/" Y) = X ` by LATTICES:11;
then  (Top L) "/\" ((X `) "\/" Y) = X ` by LATTICES:21;
then  ((X `) "\/" Y) ` = X by LATTICES:22;
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  (X "\/" Y) \ Y = X by A1; ::_thesis: verum
end;

theorem :: BOOLEALG:54
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` holds
( X = Y ` & Y = X ` )
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` holds
( X = Y ` & Y = X ` )
let X, Y be Element of L; ::_thesis: ( (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` implies ( X = Y ` & Y = X ` ) )
assume that
A1: (X `) "\/" (Y `) = X "\/" Y and
A2: X misses X ` and
A3: Y misses Y ` ; ::_thesis: ( X = Y ` & Y = X ` )
A4: X "/\" (X `) = Bottom L by A2, Def4;
A5: Y "/\" (Y `) = Bottom L by A3, Def4;
then B6: (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, LATTICES:14;
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, LATTICES:14
.= X by LATTICES:def_9 ;
hence  X = Y ` by B6, LATTICES:def_9; ::_thesis: Y = X `
 (X `) "/\" ((X `) "\/" (Y `)) = (Bottom L) "\/" ((X `) "/\" Y) by A1, A4, LATTICES:def_11;
hence  Y = X ` by A7, LATTICES:def_9; ::_thesis: verum
end;

theorem :: BOOLEALG:55
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` holds
( X = X ` & Y = Y ` )
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` holds
( X = X ` & Y = Y ` )
let X, Y be Element of L; ::_thesis: ( (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` implies ( X = X ` & Y = Y ` ) )
assume that
A1: (X `) "\/" (Y `) = X "\/" Y and
A2: Y misses X ` and
A3: X misses Y ` ; ::_thesis: ( X = X ` & Y = Y ` )
A4: Y "/\" (X `) = Bottom L by A2, Def4;
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, Def4;
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  ( X = X ` & Y = Y ` ) by A11, A9, A12, Def3; ::_thesis: verum
end;

theorem :: BOOLEALG:56
for L being B_Lattice
for X being Element of L holds X \+\ (Bottom L) = X
proof
let L be B_Lattice; ::_thesis: for X being Element of L holds X \+\ (Bottom L) = X
let X be Element of L; ::_thesis: X \+\ (Bottom L) = X
thus X \+\ (Bottom L) = X "\/" (Bottom L) by Th47
.= X ; ::_thesis: verum
end;

theorem :: BOOLEALG:57
for L being B_Lattice
for X being Element of L holds X \+\ X = Bottom L by LATTICES:20;

theorem :: BOOLEALG:58
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \+\ Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "/\" Y misses X \+\ Y
let X, Y be Element of L; ::_thesis: X "/\" Y misses X \+\ Y
 ( X "/\" Y misses X \ Y & X "/\" Y misses Y \ X ) by Th50;
hence  X "/\" Y misses X \+\ Y by Th49; ::_thesis: verum
end;

theorem :: BOOLEALG:59
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)
let X, Y be Element of L; ::_thesis: X "\/" Y = X \+\ (Y \ X)
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  X "\/" Y = X \+\ (Y \ X) ; ::_thesis: verum
end;

theorem :: BOOLEALG:60
for L being B_Lattice
for X, Y being Element of L holds X \+\ (X "/\" Y) = X \ Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X \+\ (X "/\" Y) = X \ Y
let X, Y be Element of L; ::_thesis: X \+\ (X "/\" Y) = X \ Y
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  X \+\ (X "/\" Y) = X \ Y ; ::_thesis: verum
end;

theorem :: BOOLEALG:61
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
let X, Y be Element of L; ::_thesis: X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
thus X "\/" Y = (Y \ X) "\/" X by Th35
.= (Y \ X) "\/" ((X \ Y) "\/" (X "/\" Y)) by Th36
.= (X \+\ Y) "\/" (X "/\" Y) by LATTICES:def_5 ; ::_thesis: verum
end;

Lm2:  for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
let X, Y be Element of L; ::_thesis: (X "\/" Y) \ (X \+\ Y) = X "/\" Y
set XY = X "\/" Y;
thus (X "\/" Y) \ (X \+\ Y) = (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) by LATTICES:24
.= (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:23
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:23
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X))
.= (X "\/" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))
.= ((X "\/" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) by LATTICES:def_7
.= (((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y `) "\/" X) by LATTICES:def_11
.= (((X "\/" Y) "/\" (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 ; ::_thesis: verum
end;

theorem :: BOOLEALG:62
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
let X, Y be Element of L; ::_thesis: (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
set XY = X \+\ Y;
set A = Y "/\" (X `);
(X \+\ Y) \+\ (X "/\" Y) = ((X \+\ Y) "/\" ((X `) "\/" (Y `))) "\/" ((X "/\" Y) "/\" ((X \+\ Y) `)) by LATTICES:23
.= (((X \+\ Y) "/\" (X `)) "\/" ((X \+\ Y) "/\" (Y `))) "\/" ((X "/\" Y) "/\" ((X \+\ Y) `)) by LATTICES:def_11
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `))) by LATTICES:24
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `))) by LATTICES:23
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)))) by LATTICES:23
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `))))
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)))
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((X "/\" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X)) by LATTICES:def_7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:def_11
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:def_7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((Y "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:20
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" (Y "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:def_7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((X "/\" Y) "/\" (Y `)) "\/" ((X "/\" Y) "/\" X)) by LATTICES:def_11
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" (Y "/\" (Y `))) "\/" ((X "/\" Y) "/\" X)) by LATTICES:def_7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" (Bottom L)) "\/" ((X "/\" Y) "/\" X)) by LATTICES:20
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (Y "/\" (X "/\" X)) by LATTICES:def_7
.= ((((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:def_11
.= ((((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (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
.= ((Y "/\" (X `)) "\/" (((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) by LATTICES:def_11
.= ((Y "/\" (X `)) "\/" ((X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) by LATTICES:def_7
.= ((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))))) "\/" (Y "/\" X) by LATTICES:def_7
.= ((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Bottom L)))) "\/" (Y "/\" X) by LATTICES:20
.= (Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Y "/\" X)) by LATTICES:def_5
.= (Y "/\" (X `)) "\/" (X "/\" ((Y `) "\/" Y)) by LATTICES:def_11
.= (Y "/\" (X `)) "\/" (X "/\" (Top L)) by LATTICES:21
.= (Y "\/" X) "/\" ((X `) "\/" X) by LATTICES:11
.= (Y "\/" X) "/\" (Top L) by LATTICES:21
.= Y "\/" X ;
hence  (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y ; ::_thesis: verum
end;

theorem :: BOOLEALG:63
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
let X, Y be Element of L; ::_thesis: (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
(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 Lm2 ;
hence  (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y ; ::_thesis: verum
end;

theorem Th64: :: BOOLEALG:64
for L being B_Lattice
for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)
let X, Y be Element of L; ::_thesis: X \+\ Y = (X "\/" Y) \ (X "/\" Y)
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 ; ::_thesis: verum
end;

theorem :: BOOLEALG:65
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
let X, Y, Z be Element of L; ::_thesis: (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
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 ; ::_thesis: verum
end;

theorem :: BOOLEALG:66
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)
let X, Y, Z be Element of L; ::_thesis: X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)
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  X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z) ; ::_thesis: verum
end;

theorem :: BOOLEALG:67
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
let L be B_Lattice; ::_thesis: for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
let X, Y, Z be Element of L; ::_thesis: (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
set S1 = X \ (Y "\/" Z);
set S2 = Y \ (X "\/" Z);
set S3 = Z \ (X "\/" Y);
set S4 = (X "/\" Y) "/\" Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by LATTICES:def_11
.= ((X \ (Y "\/" Z)) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ ((X "\/" Y) \ (X "/\" Y))) by Th44
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" ((Z \ (X "\/" Y)) "\/" ((X "/\" Y) "/\" Z)) by Th37
.= (((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" ((X "/\" Y) "/\" Z)) "\/" (Z \ (X "\/" Y)) by LATTICES:def_5
.= (((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ (X "\/" Y)) by LATTICES:def_5
.= ((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by LATTICES:def_5
.= ((X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by LATTICES:def_7
.= (X \ ((Y "\/" Z) \ (Y "/\" Z))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by Th37
.= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by Th44
.= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ (X "\/" Z)) "\/" ((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 ; ::_thesis: verum
end;

theorem :: BOOLEALG:68
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))
proof
let L be B_Lattice; ::_thesis: for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))
let X, Y be Element of L; ::_thesis: (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))
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 `)) ; ::_thesis: verum
end;