:: 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;