:: BOOLEALG semantic presentation

definition
let c1 be Lattice;
let c2, c3 be Element of c1;
func c2 \ c3 -> Element of a1 equals :: BOOLEALG:def 1
a2 "/\" (a3 ` );
correctness
coherence
c2 "/\" (c3 ` ) is Element of c1;
;
end;

:: deftheorem Def1 defines \ BOOLEALG:def 1 :
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \ b3 = b2 "/\" (b3 ` );

definition
let c1 be Lattice;
let c2, c3 be Element of c1;
func c2 \+\ c3 -> Element of a1 equals :: BOOLEALG:def 2
(a2 \ a3) "\/" (a3 \ a2);
correctness
coherence
(c2 \ c3) "\/" (c3 \ c2) is Element of c1;
;
end;

:: deftheorem Def2 defines \+\ BOOLEALG:def 2 :
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \+\ b3 = (b2 \ b3) "\/" (b3 \ b2);

definition
let c1 be Lattice;
let c2, c3 be Element of c1;
redefine pred = as c2 = c3 means :Def3: :: BOOLEALG:def 3
( a2 [= a3 & a3 [= a2 );
compatibility
( c2 = c3 iff ( c2 [= c3 & c3 [= c2 ) ) by LATTICES:26;
end;

:: deftheorem Def3 defines = BOOLEALG:def 3 :
for b1 being Lattice
for b2, b3 being Element of b1 holds
( b2 = b3 iff ( b2 [= b3 & b3 [= b2 ) );

definition
let c1 be Lattice;
let c2, c3 be Element of c1;
pred c2 meets c3 means :Def4: :: BOOLEALG:def 4
a2 "/\" a3 <> Bottom a1;
end;

:: deftheorem Def4 defines meets BOOLEALG:def 4 :
for b1 being Lattice
for b2, b3 being Element of b1 holds
( b2 meets b3 iff b2 "/\" b3 <> Bottom b1 );

notation
let c1 be Lattice;
let c2, c3 be Element of c1;
antonym c2 misses c3 for c2 meets c3;
end;

Lemma3: for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 & b4 [= b3 implies b2 "\/" b4 [= b3 )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
assume that
E4: c2 [= c3 and
E5: c4 [= c3 ;
E6: c2 "\/" c4 [= c3 "\/" c4 by E4, FILTER_0:1;
c3 "\/" c4 [= c3 "\/" c3 by E5, FILTER_0:1;
then c3 "\/" c4 [= c3 by LATTICES:17;
hence c2 "\/" c4 [= c3 by E6, LATTICES:25;
end;

theorem Th1: :: BOOLEALG:1
canceled;

theorem Th2: :: BOOLEALG:2
canceled;

theorem Th3: :: BOOLEALG:3
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 "\/" b3 [= b4 implies ( b2 [= b4 & b3 [= b4 ) )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
assume E4: c2 "\/" c3 [= c4 ;
then c2 "/\" (c2 "\/" c3) [= c2 "/\" c4 by LATTICES:27;
then E5: c2 [= c2 "/\" c4 by LATTICES:def 9;
E6: c2 "/\" c4 [= c4 by LATTICES:23;
c3 "/\" (c3 "\/" c2) [= c3 "/\" c4 by E4, LATTICES:27;
then E7: c3 [= c3 "/\" c4 by LATTICES:def 9;
c3 "/\" c4 [= c4 by LATTICES:23;
hence ( c2 [= c4 & c3 [= c4 ) by E5, E6, E7, LATTICES:25;
end;

theorem Th4: :: BOOLEALG:4
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds b2 "/\" b3 [= b2 "\/" b4
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
( c2 "/\" c3 [= c2 & c2 [= c2 "\/" c4 ) by LATTICES:22, LATTICES:23;
hence c2 "/\" c3 [= c2 "\/" c4 by LATTICES:25;
end;

theorem Th5: :: BOOLEALG:5
canceled;

theorem Th6: :: BOOLEALG:6
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 implies b2 \ b4 [= b3 )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
assume c2 [= c3 ;
then E4: c2 "/\" (c4 ` ) [= c3 "/\" (c4 ` ) by LATTICES:27;
c3 "/\" (c4 ` ) [= c3 by LATTICES:23;
then c2 "/\" (c4 ` ) [= c3 by E4, LATTICES:25;
hence c2 \ c4 [= c3 ;
end;

theorem Th7: :: BOOLEALG:7
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 implies b2 \ b4 [= b3 \ b4 ) by LATTICES:27;

theorem Th8: :: BOOLEALG:8
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \ b3 [= b2 by LATTICES:23;

theorem Th9: :: BOOLEALG:9
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \ b3 [= b2 \+\ b3 by LATTICES:22;

theorem Th10: :: BOOLEALG:10
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 \ b3 [= b4 & b3 \ b2 [= b4 implies b2 \+\ b3 [= b4 ) by Lemma3;

theorem Th11: :: BOOLEALG:11
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 = b3 "\/" b4 iff ( b3 [= b2 & b4 [= b2 & ( for b5 being Element of b1 holds
( b3 [= b5 & b4 [= b5 implies b2 [= b5 ) ) ) )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
thus ( c2 = c3 "\/" c4 implies ( c3 [= c2 & c4 [= c2 & ( for b1 being Element of c1 holds
( c3 [= b1 & c4 [= b1 implies c2 [= b1 ) ) ) ) by Lemma3, LATTICES:22;
assume that
E6: c3 [= c2 and
E7: c4 [= c2 and
E8: for b1 being Element of c1 holds
( c3 [= b1 & c4 [= b1 implies c2 [= b1 ) ;
( c3 [= c3 "\/" c4 & c4 [= c3 "\/" c4 ) by LATTICES:22;
then E9: c2 [= c3 "\/" c4 by E8;
c3 "\/" c4 [= c2 by E6, E7, Lemma3;
hence c2 = c3 "\/" c4 by E9, LATTICES:26;
end;

theorem Th12: :: BOOLEALG:12
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 = b3 "/\" b4 iff ( b2 [= b3 & b2 [= b4 & ( for b5 being Element of b1 holds
( b5 [= b3 & b5 [= b4 implies b5 [= b2 ) ) ) )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
thus ( c2 = c3 "/\" c4 implies ( c2 [= c3 & c2 [= c4 & ( for b1 being Element of c1 holds
( b1 [= c3 & b1 [= c4 implies b1 [= c2 ) ) ) ) by FILTER_0:7, LATTICES:23;
assume that
E6: ( c2 [= c3 & c2 [= c4 ) and
E7: for b1 being Element of c1 holds
( b1 [= c3 & b1 [= c4 implies b1 [= c2 ) ;
E8: c2 [= c3 "/\" c4 by E6, FILTER_0:7;
( c3 "/\" c4 [= c3 & c3 "/\" c4 [= c4 ) by LATTICES:23;
then c3 "/\" c4 [= c2 by E7;
hence c2 = c3 "/\" c4 by E8, Def3;
end;

theorem Th13: :: BOOLEALG:13
canceled;

theorem Th14: :: BOOLEALG:14
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds b2 "/\" (b3 \ b4) = (b2 "/\" b3) \ b4 by LATTICES:def 7;

theorem Th15: :: BOOLEALG:15
for b1 being Lattice
for b2, b3 being Element of b1 holds
( b2 meets b3 implies b3 meets b2 )
proof
let c1 be Lattice;
let c2, c3 be Element of c1;
assume c2 meets c3 ;
then c2 "/\" c3 <> Bottom c1 by Def4;
hence c3 meets c2 by Def4;
end;

theorem Th16: :: BOOLEALG:16
for b1 being Lattice
for b2 being Element of b1 holds
( b2 meets b2 iff b2 <> Bottom b1 )
proof
let c1 be Lattice;
let c2 be Element of c1;
hereby
assume c2 meets c2 ;
then c2 "/\" c2 <> Bottom c1 by Def4;
hence c2 <> Bottom c1 by LATTICES:18;
end;
assume E8: c2 <> Bottom c1 ;
c2 "/\" c2 = c2 by LATTICES:18;
hence c2 meets c2 by E8, Def4;
end;

theorem Th17: :: BOOLEALG:17
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \+\ b3 = b3 \+\ b2 ;

definition
let c1 be Lattice;
let c2, c3 be Element of c1;
redefine pred meets as c2 meets c3;
symmetry
for b1, b2 being Element of c1 holds
( b1 meets b2 implies b2 meets b1 ) by Th15;
redefine func \+\ as c2 \+\ c3 -> Element of a1;
commutativity
for b1, b2 being Element of c1 holds b1 \+\ b2 = b2 \+\ b1 ;
end;

theorem Th18: :: BOOLEALG:18
canceled;

theorem Th19: :: BOOLEALG:19
canceled;

theorem Th20: :: BOOLEALG:20
canceled;

theorem Th21: :: BOOLEALG:21
for b1 being M_Lattice
for b2, b3 being Element of b1 holds
not ( b2 misses b3 & not b3 misses b2 )
proof
let c1 be M_Lattice;
let c2, c3 be Element of c1;
assume c2 misses c3 ;
then c3 "/\" c2 = Bottom c1 by Def4;
hence c3 misses c2 by Def4;
end;

theorem Th22: :: BOOLEALG:22
for b1 being D_Lattice
for b2, b3, b4 being Element of b1 holds
( (b2 "/\" b3) "\/" (b2 "/\" b4) = b2 implies b2 [= b3 "\/" b4 )
proof
let c1 be D_Lattice;
let c2, c3, c4 be Element of c1;
assume (c2 "/\" c3) "\/" (c2 "/\" c4) = c2 ;
then c2 "/\" (c3 "\/" c4) = c2 by LATTICES:def 11;
hence c2 [= c3 "\/" c4 by LATTICES:21;
end;

theorem Th23: :: BOOLEALG:23
canceled;

theorem Th24: :: BOOLEALG:24
for b1 being D_Lattice
for b2, b3, b4 being Element of b1 holds (b2 "\/" b3) \ b4 = (b2 \ b4) "\/" (b3 \ b4) by LATTICES:def 11;

theorem Th25: :: BOOLEALG:25
for b1 being 0_Lattice
for b2 being Element of b1 holds
( b2 [= Bottom b1 implies b2 = Bottom b1 )
proof
let c1 be 0_Lattice;
let c2 be Element of c1;
assume E10: c2 [= Bottom c1 ;
Bottom c1 [= c2 by LATTICES:41;
hence c2 = Bottom c1 by E10, LATTICES:26;
end;

theorem Th26: :: BOOLEALG:26
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 & b2 [= b4 & b3 "/\" b4 = Bottom b1 implies b2 = Bottom b1 )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume that
E10: c2 [= c3 and
E11: c2 [= c4 and
E12: c3 "/\" c4 = Bottom c1 ;
c2 [= Bottom c1 by E10, E11, E12, FILTER_0:7;
hence c2 = Bottom c1 by Th25;
end;

theorem Th27: :: BOOLEALG:27
for b1 being 0_Lattice
for b2, b3 being Element of b1 holds
( b2 "\/" b3 = Bottom b1 iff ( b2 = Bottom b1 & b3 = Bottom b1 ) )
proof
let c1 be 0_Lattice;
let c2, c3 be Element of c1;
thus ( c2 "\/" c3 = Bottom c1 implies ( c2 = Bottom c1 & c3 = Bottom c1 ) )
proof
assume E11: c2 "\/" c3 = Bottom c1 ;
then E12: ( c2 [= Bottom c1 & Bottom c1 [= c2 ) by LATTICES:22, LATTICES:41;
( c3 [= Bottom c1 & Bottom c1 [= c3 ) by E11, LATTICES:22, LATTICES:41;
hence ( c2 = Bottom c1 & c3 = Bottom c1 ) by E12, Def3;
end;
thus ( c2 = Bottom c1 & c3 = Bottom c1 implies c2 "\/" c3 = Bottom c1 ) by LATTICES:39;
end;

theorem Th28: :: BOOLEALG:28
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 & b3 "/\" b4 = Bottom b1 implies b2 "/\" b4 = Bottom b1 )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume c2 [= c3 ;
then c2 "/\" c4 [= c3 "/\" c4 by LATTICES:27;
hence not ( c3 "/\" c4 = Bottom c1 & not c2 "/\" c4 = Bottom c1 ) by Th25;
end;

theorem Th29: :: BOOLEALG:29
for b1 being 0_Lattice
for b2 being Element of b1 holds (Bottom b1) \ b2 = Bottom b1 by LATTICES:40;

theorem Th30: :: BOOLEALG:30
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 meets b3 & b3 [= b4 implies b2 meets b4 )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume that
E13: c2 meets c3 and
E14: c3 [= c4 ;
E15: c2 "/\" c3 <> Bottom c1 by E13, Def4;
c2 "/\" c3 [= c2 "/\" c4 by E14, LATTICES:27;
then c2 "/\" c4 <> Bottom c1 by E15, Th25;
hence c2 meets c4 by Def4;
end;

theorem Th31: :: BOOLEALG:31
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 meets b3 "/\" b4 implies ( b2 meets b3 & b2 meets b4 ) )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume c2 meets c3 "/\" c4 ;
then E14: c2 "/\" (c3 "/\" c4) <> Bottom c1 by Def4;
then E15: (c2 "/\" c3) "/\" c4 <> Bottom c1 by LATTICES:def 7;
(c2 "/\" c4) "/\" c3 <> Bottom c1 by E14, LATTICES:def 7;
then ( c2 "/\" c3 <> Bottom c1 & c2 "/\" c4 <> Bottom c1 ) by E15, LATTICES:40;
hence ( c2 meets c3 & c2 meets c4 ) by Def4;
end;

theorem Th32: :: BOOLEALG:32
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 meets b3 \ b4 implies b2 meets b3 )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume c2 meets c3 \ c4 ;
then c2 "/\" (c3 \ c4) <> Bottom c1 by Def4;
then c2 "/\" (c3 "/\" (c4 ` )) <> Bottom c1 ;
then (c2 "/\" c3) "/\" (c4 ` ) <> Bottom c1 by LATTICES:def 7;
then c2 "/\" c3 <> Bottom c1 by LATTICES:40;
hence c2 meets c3 by Def4;
end;

theorem Th33: :: BOOLEALG:33
for b1 being 0_Lattice
for b2 being Element of b1 holds
b2 misses Bottom b1
proof
let c1 be 0_Lattice;
let c2 be Element of c1;
assume c2 meets Bottom c1 ;
then c2 "/\" (Bottom c1) <> Bottom c1 by Def4;
hence not verum by LATTICES:40;
end;

theorem Th34: :: BOOLEALG:34
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
not ( b2 misses b3 & b4 [= b3 & not b2 misses b4 ) by Th30;

theorem Th35: :: BOOLEALG:35
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
not ( not ( not b2 misses b3 & not b2 misses b4 ) & not b2 misses b3 "/\" b4 ) by Th31;

theorem Th36: :: BOOLEALG:36
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 & b2 [= b4 & b3 misses b4 implies b2 = Bottom b1 )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume ( c2 [= c3 & c2 [= c4 & c3 misses c4 ) ;
then ( c2 [= c3 "/\" c4 & c3 "/\" c4 = Bottom c1 ) by Def4, FILTER_0:7;
hence c2 = Bottom c1 by Th25;
end;

theorem Th37: :: BOOLEALG:37
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 misses b3 implies ( b4 "/\" b2 misses b4 "/\" b3 & b2 "/\" b4 misses b3 "/\" b4 ) )
proof
let c1 be 0_Lattice;
let c2, c3, c4 be Element of c1;
assume E14: c2 misses c3 ;
thus c4 "/\" c2 misses c4 "/\" c3
proof
(c4 "/\" c2) "/\" (c4 "/\" c3) = c4 "/\" (c2 "/\" (c3 "/\" c4)) by LATTICES:def 7
.= c4 "/\" ((c2 "/\" c3) "/\" c4) by LATTICES:def 7
.= c4 "/\" ((Bottom c1) "/\" c4) by E14, Def4
.= c4 "/\" (Bottom c1) by LATTICES:40
.= Bottom c1 by LATTICES:40 ;
hence c4 "/\" c2 misses c4 "/\" c3 by Def4;
end;
hence c2 "/\" c4 misses c3 "/\" c4 ;
end;

theorem Th38: :: BOOLEALG:38
for b1 being B_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 \ b3 [= b4 implies b2 [= b3 "\/" b4 )
proof
let c1 be B_Lattice;
let c2, c3, c4 be Element of c1;
assume c2 \ c3 [= c4 ;
then c2 "/\" (c3 ` ) [= c4 ;
then c3 "\/" (c2 "/\" (c3 ` )) [= c3 "\/" c4 by FILTER_0:1;
then (c3 "\/" c2) "/\" (c3 "\/" (c3 ` )) [= c3 "\/" c4 by LATTICES:31;
then (c3 "\/" c2) "/\" (Top c1) [= c3 "\/" c4 by LATTICES:48;
then E14: c2 "\/" c3 [= c3 "\/" c4 by LATTICES:43;
c2 [= c2 "\/" c3 by LATTICES:22;
hence c2 [= c3 "\/" c4 by E14, LATTICES:25;
end;

theorem Th39: :: BOOLEALG:39
for b1 being B_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 implies b4 \ b3 [= b4 \ b2 )
proof
let c1 be B_Lattice;
let c2, c3, c4 be Element of c1;
assume c2 [= c3 ;
then E15: c3 ` [= c2 ` by LATTICES:53;
thus c4 \ c3 [= c4 \ c2 by E15, LATTICES:27;
end;

theorem Th40: :: BOOLEALG:40
for b1 being B_Lattice
for b2, b3, b4, b5 being Element of b1 holds
( b2 [= b3 & b4 [= b5 implies b2 \ b5 [= b3 \ b4 )
proof
let c1 be B_Lattice;
let c2, c3, c4, c5 be Element of c1;
assume that
E15: c2 [= c3 and
E16: c4 [= c5 ;
E17: c2 \ c5 [= c3 \ c5 by E15, Th7;
c3 \ c5 [= c3 \ c4 by E16, Th39;
hence c2 \ c5 [= c3 \ c4 by E17, LATTICES:25;
end;

theorem Th41: :: BOOLEALG:41
for b1 being B_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 "\/" b4 implies ( b2 \ b3 [= b4 & b2 \ b4 [= b3 ) )
proof
let c1 be B_Lattice;
let c2, c3, c4 be Element of c1;
assume E15: c2 [= c3 "\/" c4 ;
thus c2 \ c3 [= c4
proof
c2 "/\" (c3 ` ) [= (c3 "\/" c4) "/\" (c3 ` ) by E15, LATTICES:27;
then c2 "/\" (c3 ` ) [= (c3 "/\" (c3 ` )) "\/" (c4 "/\" (c3 ` )) by LATTICES:def 11;
then c2 \ c3 [= (c3 "/\" (c3 ` )) "\/" (c4 "/\" (c3 ` )) ;
then c2 \ c3 [= (Bottom c1) "\/" (c4 "/\" (c3 ` )) by LATTICES:47;
then E16: c2 \ c3 [= c4 "/\" (c3 ` ) by LATTICES:39;
c4 "/\" (c3 ` ) [= c4 by LATTICES:23;
hence c2 \ c3 [= c4 by E16, LATTICES:25;
end;
c2 "/\" (c4 ` ) [= (c3 "\/" c4) "/\" (c4 ` ) by E15, LATTICES:27;
then c2 "/\" (c4 ` ) [= (c3 "/\" (c4 ` )) "\/" (c4 "/\" (c4 ` )) by LATTICES:def 11;
then c2 \ c4 [= (c3 "/\" (c4 ` )) "\/" (c4 "/\" (c4 ` )) ;
then c2 \ c4 [= (c3 "/\" (c4 ` )) "\/" (Bottom c1) by LATTICES:47;
then E16: c2 \ c4 [= c3 "/\" (c4 ` ) by LATTICES:39;
c3 "/\" (c4 ` ) [= c3 by LATTICES:23;
hence c2 \ c4 [= c3 by E16, LATTICES:25;
end;

theorem Th42: :: BOOLEALG:42
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 ` [= (b2 "/\" b3) ` & b3 ` [= (b2 "/\" b3) ` )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
E15: c2 ` [= (c2 ` ) "\/" (c3 ` ) by LATTICES:22;
c3 ` [= (c2 ` ) "\/" (c3 ` ) by LATTICES:22;
hence ( c2 ` [= (c2 "/\" c3) ` & c3 ` [= (c2 "/\" c3) ` ) by E15, LATTICES:50;
end;

theorem Th43: :: BOOLEALG:43
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( (b2 "\/" b3) ` [= b2 ` & (b2 "\/" b3) ` [= b3 ` )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
thus (c2 "\/" c3) ` [= c2 `
proof
(c2 "\/" c3) ` = (c2 ` ) "/\" (c3 ` ) by LATTICES:51;
hence (c2 "\/" c3) ` [= c2 ` by LATTICES:23;
end;
(c2 "\/" c3) ` = (c3 ` ) "/\" (c2 ` ) by LATTICES:51;
hence (c2 "\/" c3) ` [= c3 ` by LATTICES:23;
end;

theorem Th44: :: BOOLEALG:44
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 [= b3 \ b2 implies b2 = Bottom b1 )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
assume c2 [= c3 \ c2 ;
then E15: c2 [= c3 "/\" (c2 ` ) ;
c2 "/\" (c3 "/\" (c2 ` )) = c3 "/\" ((c2 ` ) "/\" c2) by LATTICES:def 7
.= c3 "/\" (Bottom c1) by LATTICES:47
.= Bottom c1 by LATTICES:40 ;
hence c2 = Bottom c1 by E15, LATTICES:21;
end;

theorem Th45: :: BOOLEALG:45
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 [= b3 implies b3 = b2 "\/" (b3 \ b2) )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
assume E15: c2 [= c3 ;
c3 = c3 "/\" (Top c1) by LATTICES:43
.= c3 "/\" (c2 "\/" (c2 ` )) by LATTICES:48
.= (c3 "/\" c2) "\/" (c3 "/\" (c2 ` )) by LATTICES:def 11
.= c2 "\/" (c3 "/\" (c2 ` )) by E15, LATTICES:21
.= c2 "\/" (c3 \ c2) ;
hence c3 = c2 "\/" (c3 \ c2) ;
end;

theorem Th46: :: BOOLEALG:46
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 \ b3 = Bottom b1 iff b2 [= b3 )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
thus ( c2 \ c3 = Bottom c1 implies c2 [= c3 )
proof
assume E16: c2 \ c3 = Bottom c1 ;
( c2 "/\" (c3 ` ) = Bottom c1 implies c2 [= (c3 ` ) ` ) by LATTICES:52;
hence c2 [= c3 by E16, LATTICES:49;
end;
assume c2 [= c3 ;
then c2 "/\" (c3 ` ) [= (c3 ` ) "/\" c3 by LATTICES:27;
then c2 "/\" (c3 ` ) [= Bottom c1 by LATTICES:47;
then E16: c2 \ c3 [= Bottom c1 ;
Bottom c1 [= c2 \ c3 by LATTICES:41;
hence c2 \ c3 = Bottom c1 by E16, Def3;
end;

theorem Th47: :: BOOLEALG:47
for b1 being B_Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 "\/" b4 & b2 "/\" b4 = Bottom b1 implies b2 [= b3 )
proof
let c1 be B_Lattice;
let c2, c3, c4 be Element of c1;
assume that
E16: c2 [= c3 "\/" c4 and
E17: c2 "/\" c4 = Bottom c1 ;
c2 "/\" (c3 "\/" c4) = c2 by E16, LATTICES:21;
then (c2 "/\" c3) "\/" (Bottom c1) = c2 by E17, LATTICES:def 11;
then c2 "/\" c3 = c2 by LATTICES:39;
hence c2 [= c3 by LATTICES:21;
end;

theorem Th48: :: BOOLEALG:48
for b1 being B_Lattice
for b2, b3 being Element of b1 holds b2 "\/" b3 = (b2 \ b3) "\/" b3
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
thus c2 "\/" c3 = (c2 "\/" c3) "/\" (Top c1) by LATTICES:43
.= (c2 "\/" c3) "/\" ((c3 ` ) "\/" c3) by LATTICES:48
.= (c2 "/\" (c3 ` )) "\/" c3 by LATTICES:31
.= (c2 \ c3) "\/" c3 ;
end;

theorem Th49: :: BOOLEALG:49
for b1 being B_Lattice
for b2, b3 being Element of b1 holds b2 \ (b2 "\/" b3) = Bottom b1
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
( c2 [= c2 "\/" c3 & c2 [= c3 "\/" c2 ) by LATTICES:22;
hence c2 \ (c2 "\/" c3) = Bottom c1 by Th46;
end;

theorem Th50: :: BOOLEALG:50
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 \ (b2 "/\" b3) = b2 \ b3 & b2 \ (b3 "/\" b2) = b2 \ b3 )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
thus c2 \ (c2 "/\" c3) = c2 \ c3
proof
c2 \ (c2 "/\" c3) = c2 "/\" ((c2 "/\" c3) ` )
.= c2 "/\" ((c2 ` ) "\/" (c3 ` )) by LATTICES:50
.= (c2 "/\" (c2 ` )) "\/" (c2 "/\" (c3 ` )) by LATTICES:def 11
.= (Bottom c1) "\/" (c2 "/\" (c3 ` )) by LATTICES:47
.= c2 "/\" (c3 ` ) by LATTICES:39 ;
hence c2 \ (c2 "/\" c3) = c2 \ c3 ;
end;
c2 \ (c3 "/\" c2) = c2 "/\" ((c3 "/\" c2) ` )
.= c2 "/\" ((c3 ` ) "\/" (c2 ` )) by LATTICES:50
.= (c2 "/\" (c3 ` )) "\/" (c2 "/\" (c2 ` )) by LATTICES:def 11
.= (c2 "/\" (c3 ` )) "\/" (Bottom c1) by LATTICES:47
.= c2 "/\" (c3 ` ) by LATTICES:39 ;
hence c2 \ (c3 "/\" c2) = c2 \ c3 ;
end;

theorem Th51: :: BOOLEALG:51
for b1 being B_Lattice
for b2, b3 being Element of b1 holds (b2 \ b3) "/\" b3 = Bottom b1
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
(c2 \ c3) "/\" c3 = (c2 "/\" (c3 ` )) "/\" c3
.= c2 "/\" ((c3 ` ) "/\" c3) by LATTICES:def 7
.= c2 "/\" (Bottom c1) by LATTICES:47 ;
hence (c2 \ c3) "/\" c3 = Bottom c1 by LATTICES:40;
end;

theorem Th52: :: BOOLEALG:52
for b1 being B_Lattice
for b2, b3 being Element of b1 holds
( b2 "\/" (b3 \ b2) = b2 "\/" b3 & (b3 \ b2) "\/" b2 = b3 "\/" b2 )
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
thus c2 "\/" (c3 \ c2) = c2 "\/" c3
proof
c2 "\/" (c3 \ c2) = c2 "\/" (c3 "/\" (c2 ` ))
.= (c2 "\/" c3) "/\" (c2 "\/" (c2 ` )) by LATTICES:31
.= (c2 "\/" c3) "/\" (Top c1) by LATTICES:48 ;
hence c2 "\/" (c3 \ c2) = c2 "\/" c3 by LATTICES:43;
end;
(c3 \ c2) "\/" c2 = (c3 "/\" (c2 ` )) "\/" c2
.= (c3 "\/" c2) "/\" ((c2 ` ) "\/" c2) by LATTICES:31
.= (c3 "\/" c2) "/\" (Top c1) by LATTICES:48 ;
hence (c3 \ c2) "\/" c2 = c3 "\/" c2 by LATTICES:43;
end;

theorem Th53: :: BOOLEALG:53
for b1 being B_Lattice
for b2, b3 being Element of b1 holds (b2 "/\" b3) "\/" (b2 \ b3) = b2
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
(c2 "/\" c3) "\/" (c2 \ c3) = (c2 "/\" c3) "\/" (c2 "/\" (c3 ` ))
.= ((c2 "/\" c3) "\/" c2) "/\" ((c2 "/\" c3) "\/" (c3 ` )) by LATTICES:31
.= c2 "/\" ((c2 "/\" c3) "\/" (c3 ` )) by LATTICES:def 8
.= c2 "/\" ((c2 "\/" (c3 ` )) "/\" (c3 "\/" (c3 ` ))) by LATTICES:31
.= c2 "/\" ((c2 "\/" (c3 ` )) "/\" (Top c1)) by LATTICES:48
.= c2 "/\" (c2 "\/" (c3 ` )) by LATTICES:43
.= c2 by LATTICES:def 9 ;
hence (c2 "/\" c3) "\/" (c2 \ c3) = c2 ;
end;

theorem Th54: :: BOOLEALG:54
for b1 being B_Lattice
for b2, b3, b4 being Element of b1 holds b2 \ (b3 \ b4) = (b2 \ b3) "\/" (b2 "/\" b4)
proof
let c1 be B_Lattice;
let c2, c3, c4 be Element of c1;
c2 \ (c3 \ c4) = c2 \ (c3 "/\" (c4 ` ))
.= c2 "/\" ((c3 "/\" (c4 ` )) ` )
.= c2 "/\" ((c3 ` ) "\/" ((c4 ` ) ` )) by LATTICES:50
.= c2 "/\" ((c3 ` ) "\/" c4) by LATTICES:49
.= (c2 "/\" (c3 ` )) "\/" (c2 "/\" c4) by LATTICES:def 11 ;
hence c2 \ (c3 \ c4) = (c2 \ c3) "\/" (c2 "/\" c4) ;
end;

theorem Th55: :: BOOLEALG:55
for b1 being B_Lattice
for b2, b3 being Element of b1 holds b2 \ (b2 \ b3) = b2 "/\" b3
proof
let c1 be B_Lattice;
let c2, c3 be Element of c1;
c2 \ (c2 \ c3) = c2 "/\" ((c2 \ c3) ` )
.= c2 "/\" ((c2 "/\" (c3 ` )) ` )
.= c2 "/\" ((c2 ` ) "\/" ((c3 ` ) ` )) by LATTICES:50
.= c2 "/\" ((c2 ` ) "\/" c3) by LATTICES:49
.= (c2 "/\" (c2 ` )) "\/" (c2 "/\