:: BOOLEALG semantic presentation

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

:: deftheorem 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 a2 \+\ a3 -> Element of a1 equals :: BOOLEALG:def 2
(a2 \ a3) "\/" (a3 \ a2);
correctness
coherence
(c2 \ c3) "\/" (c3 \ c2) is Element of c1;
;
end;

:: deftheorem 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 a2 = a3 means :E1: :: BOOLEALG:def 3
( a2 [= a3 & a3 [= a2 );
compatibility
( c2 = c3 iff ( c2 [= c3 & c3 [= c2 ) ) by LATTICES:26;
end;

:: deftheorem E1 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 a2 meets a3 means :E2: :: BOOLEALG:def 4
a2 "/\" a3 <> Bottom a1;
end;

:: deftheorem E2 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;
end;

E3: 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 :: BOOLEALG:1
canceled;

theorem :: BOOLEALG:2
canceled;

theorem :: 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 :: 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 :: BOOLEALG:5
canceled;

theorem :: 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 E4: :: BOOLEALG:7
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 [= b3 implies b2 \ b4 [= b3 \ b4 )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
assume E5: c2 [= c3 ;
( c2 "/\" (c4 ` ) = c2 \ c4 & c3 "/\" (c4 ` ) = c3 \ c4 ) ;
hence c2 \ c4 [= c3 \ c4 by E5, LATTICES:27;
end;

theorem E5: :: BOOLEALG:8
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \ b3 [= b2
proof
let c1 be Lattice;
let c2, c3 be Element of c1;
c2 "/\" (c3 ` ) [= c2 by LATTICES:23;
hence c2 \ c3 [= c2 ;
end;

theorem :: BOOLEALG:9
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \ b3 [= b2 \+\ b3
proof
let c1 be Lattice;
let c2, c3 be Element of c1;
c2 \+\ c3 = (c2 \ c3) "\/" (c3 \ c2) ;
hence c2 \ c3 [= c2 \+\ c3 by LATTICES:22;
end;

theorem :: 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 ) )
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
assume that E6: c2 \ c3 [= c4
and E7: c3 \ c2 [= c4 ;
(c2 \ c3) "\/" (c3 \ c2) [= c4 by E6, E7, E3;
hence c2 \+\ c3 [= c4 ;
end;

theorem :: 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 E3, 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, E3;
hence c2 = c3 "\/" c4 by E9, LATTICES:26;
end;

theorem :: 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, E1;
end;

theorem :: BOOLEALG:13
canceled;

theorem E6: :: BOOLEALG:14
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds b2 "/\" (b3 \ b4) = (b2 "/\" b3) \ b4
proof
let c1 be Lattice;
let c2, c3, c4 be Element of c1;
c2 "/\" (c3 \ c4) = c2 "/\" (c3 "/\" (c4 ` ))
.= (c2 "/\" c3) "/\" (c4 ` ) by LATTICES:def 7
.= (c2 "/\" c3) \ c4 ;
hence c2 "/\" (c3 \ c4) = (c2 "/\" c3) \ c4 ;
end;

theorem E7: :: 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 E2;
hence c3 meets c2 by E2;
end;

theorem :: 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 E2;
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, E2;
end;

theorem :: BOOLEALG:17
for b1 being Lattice
for b2, b3 being Element of b1 holds b2 \+\ b3 = b3 \+\ b2
proof
let c1 be Lattice;
let c2, c3 be Element of c1;
thus c2 \+\ c3 = (c2 \ c3) "\/" (c3 \ c2)
.= c3 \+\ c2 ;
end;

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

theorem :: BOOLEALG:18
canceled;

theorem :: BOOLEALG:19
canceled;

theorem :: BOOLEALG:20
canceled;

theorem :: 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 E2;
hence c3 misses c2 by E2;
end;

theorem :: 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 :: BOOLEALG:23
canceled;

theorem E8: :: BOOLEALG:24
for b1 being D_Lattice
for b2, b3, b4 being Element of b1 holds (b2 "\/" b3) \ b4 = (b2 \ b4) "\/" (b3 \ b4)
proof
let c1 be D_Lattice;
let c2, c3, c4 be Element of c1;
thus (c2 "\/" c3) \ c4 = (c2 "\/" c3) "/\" (c4 ` )
.= (c2 "/\" (c4 ` )) "\/" (c3 "/\" (c4 ` )) by LATTICES:def 11
.= (c2 \ c4) "\/" (c3 "/\" (c4 ` ))
.= (c2 \ c4) "\/" (c3 \ c4) ;
end;

theorem E9: :: 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 :: 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 E9;
end;

theorem E10: :: 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, E1;
end;
thus ( ( c2 = Bottom c1 & c3 = Bottom c1 ) implies ( c2 "\/" c3 = Bottom c1 ) ) by LATTICES:39;
end;

theorem :: 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 E9;
end;

theorem E11: :: BOOLEALG:29
for b1 being 0_Lattice
for b2 being Element of b1 holds (Bottom b1) \ b2 = Bottom b1
proof
let c1 be 0_Lattice;
let c2 be Element of c1;
(Bottom c1) \ c2 = (Bottom c1) "/\" (c2 ` )
.= Bottom c1 by LATTICES:40 ;
hence (Bottom c1) \ c2 = Bottom c1 ;
end;

theorem E12: :: 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, E2;
c2 "/\" c3 [= c2 "/\" c4 by E14, LATTICES:27;
then c2 "/\" c4 <> Bottom c1 by E15, E9;
hence c2 meets c4 by E2;
end;

theorem E13: :: 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 E2;
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 E2;
end;

theorem :: 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 E2;
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 E2;
end;

theorem :: 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 E2;
hence not verum by LATTICES:40;
end;

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

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

theorem :: BOOLEALG:36
for b1 being 0_Lattice
for b2, b3, b4 being Element of b1 holds
( ( b2 [= b3 & b2 [= b4 ) implies ( not b3 misses b4 or 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 E2, FILTER_0:7;
hence c2 = Bottom c1 by E9;
end;

theorem :: 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, E2
.= c4 "/\" (Bottom c1) by LATTICES:40
.= Bottom c1 by LATTICES:40 ;
hence c4 "/\" c2 misses c4 "/\" c3 by E2;
end;
hence c2 "/\" c4 misses c3 "/\" c4 ;
end;

theorem :: 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 E14: :: 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;
( c4 \ c3 = c4 "/\" (c3 ` ) & c4 "/\" (c2 ` ) = c4 \ c2 ) ;
hence c4 \ c3 [= c4 \ c2 by E15, LATTICES:27;
end;

theorem :: 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, E4;
c3 \ c5 [= c3 \ c4 by E16, E14;
hence c2 \ c5 [= c3 \ c4 by E17, LATTICES:25;
end;

theorem :: 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 :: 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 :: 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 :: 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 :: 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 E15: :: 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, E1;
end;

theorem :: 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 :: 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 :: 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 E15;
end;

theorem E16: :: 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 :: 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 E17: :: 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 E18: :: 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 E19: :: 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 :: 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 "/\" c3) by LATTICES:def 11
.= (Bottom c1) "\/" (