:: YELLOW_5 semantic presentation

begin

theorem :: YELLOW_5:1
for L being reflexive antisymmetric with_suprema RelStr
for a being Element of L holds a "\/" a = a
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for a being Element of L holds a "\/" a = a
let a be Element of L; ::_thesis: a "\/" a = a
 a <= a ;
then  ( a <= a "\/" a & a "\/" a <= a ) by YELLOW_0:22;
hence  a "\/" a = a by YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th2: :: YELLOW_5:2
for L being reflexive antisymmetric with_infima RelStr
for a being Element of L holds a "/\" a = a
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for a being Element of L holds a "/\" a = a
let a be Element of L; ::_thesis: a "/\" a = a
 a <= a ;
then  ( a "/\" a <= a & a <= a "/\" a ) by YELLOW_0:23;
hence  a "/\" a = a by YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: YELLOW_5:3
for L being transitive antisymmetric with_suprema RelStr
for a, b, c being Element of L st a "\/" b <= c holds
a <= c
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c being Element of L st a "\/" b <= c holds
a <= c
let a, b, c be Element of L; ::_thesis: ( a "\/" b <= c implies a <= c )
A1: a <= a "\/" b by YELLOW_0:22;
assume  a "\/" b <= c ; ::_thesis: a <= c
hence  a <= c by A1, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_5:4
for L being transitive antisymmetric with_infima RelStr
for a, b, c being Element of L st c <= a "/\" b holds
c <= a
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b, c being Element of L st c <= a "/\" b holds
c <= a
let a, b, c be Element of L; ::_thesis: ( c <= a "/\" b implies c <= a )
A1: a "/\" b <= a by YELLOW_0:23;
assume  c <= a "/\" b ; ::_thesis: c <= a
hence  c <= a by A1, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_5:5
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L holds a "/\" b <= a "\/" c
proof
let L be transitive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for a, b, c being Element of L holds a "/\" b <= a "\/" c
let a, b, c be Element of L; ::_thesis: a "/\" b <= a "\/" c
 ( a "/\" b <= a & a <= a "\/" c ) by YELLOW_0:22, YELLOW_0:23;
hence  a "/\" b <= a "\/" c by YELLOW_0:def_2; ::_thesis: verum
end;

theorem Th6: :: YELLOW_5:6
for L being transitive antisymmetric with_infima RelStr
for a, b, c being Element of L st a <= b holds
a "/\" c <= b "/\" c
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b, c being Element of L st a <= b holds
a "/\" c <= b "/\" c
let a, b, c be Element of L; ::_thesis: ( a <= b implies a "/\" c <= b "/\" c )
A1: a "/\" c <= a by YELLOW_0:23;
A2: a "/\" c <= c by YELLOW_0:23;
assume  a <= b ; ::_thesis: a "/\" c <= b "/\" c
then  a "/\" c <= b by A1, YELLOW_0:def_2;
hence  a "/\" c <= b "/\" c by A2, YELLOW_0:23; ::_thesis: verum
end;

theorem Th7: :: YELLOW_5:7
for L being transitive antisymmetric with_suprema RelStr
for a, b, c being Element of L st a <= b holds
a "\/" c <= b "\/" c
proof
let L be non empty transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c being Element of L st a <= b holds
a "\/" c <= b "\/" c
let a, b, c be Element of L; ::_thesis: ( a <= b implies a "\/" c <= b "\/" c )
A1: b <= b "\/" c by YELLOW_0:22;
A2: c <= b "\/" c by YELLOW_0:22;
assume  a <= b ; ::_thesis: a "\/" c <= b "\/" c
then  a <= b "\/" c by A1, YELLOW_0:def_2;
hence  a "\/" c <= b "\/" c by A2, YELLOW_0:22; ::_thesis: verum
end;

theorem Th8: :: YELLOW_5:8
for L being sup-Semilattice
for a, b being Element of L st a <= b holds
a "\/" b = b
proof
let L be sup-Semilattice; ::_thesis: for a, b being Element of L st a <= b holds
a "\/" b = b
let a, b be Element of L; ::_thesis: ( a <= b implies a "\/" b = b )
A1: b <= b ;
assume  a <= b ; ::_thesis: a "\/" b = b
then  ( b <= a "\/" b & a "\/" b <= b ) by A1, YELLOW_0:22;
hence  a "\/" b = b by YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th9: :: YELLOW_5:9
for L being sup-Semilattice
for a, b, c being Element of L st a <= c & b <= c holds
a "\/" b <= c
proof
let L be sup-Semilattice; ::_thesis: for a, b, c being Element of L st a <= c & b <= c holds
a "\/" b <= c
let a, b, c be Element of L; ::_thesis: ( a <= c & b <= c implies a "\/" b <= c )
assume that
A1: a <= c and
A2: b <= c ; ::_thesis: a "\/" b <= c
 c "\/" b = c by A2, Th8;
hence  a "\/" b <= c by A1, Th7; ::_thesis: verum
end;

theorem Th10: :: YELLOW_5:10
for L being Semilattice
for a, b being Element of L st b <= a holds
a "/\" b = b
proof
let L be Semilattice; ::_thesis: for a, b being Element of L st b <= a holds
a "/\" b = b
let a, b be Element of L; ::_thesis: ( b <= a implies a "/\" b = b )
assume  b <= a ; ::_thesis: a "/\" b = b
then  b "/\" b <= a "/\" b by Th6;
then  ( a "/\" b <= b & b <= a "/\" b ) by Th2, YELLOW_0:23;
hence  a "/\" b = b by YELLOW_0:def_3; ::_thesis: verum
end;

begin

theorem Th11: :: YELLOW_5:11
for L being Boolean LATTICE
for x, y being Element of L holds
( y is_a_complement_of x iff y = 'not' x )
proof
let L be Boolean LATTICE; ::_thesis: for x, y being Element of L holds
( y is_a_complement_of x iff y = 'not' x )
let x, y be Element of L; ::_thesis: ( y is_a_complement_of x iff y = 'not' x )
A1: for x being Element of L holds 'not' ('not' x) = x by WAYBEL_1:87;
then A2: 'not' x is_a_complement_of x by WAYBEL_1:86;
then A3: x "/\" ('not' x) = Bottom L by WAYBEL_1:def_23;
A4: x "\/" ('not' x) = Top L by A2, WAYBEL_1:def_23;
hereby  ::_thesis: ( y = 'not' x implies y is_a_complement_of x )
assume A5: y is_a_complement_of x ; ::_thesis: y = 'not' x
then A6: x "/\" y = Bottom L by WAYBEL_1:def_23;
A7: Top L >= 'not' x by YELLOW_0:45;
A8: Bottom L <= y "/\" ('not' x) by YELLOW_0:44;
 Top L >= y by YELLOW_0:45;
then A9: y = (x "\/" ('not' x)) "/\" y by A4, YELLOW_0:25
.= (x "/\" y) "\/" (y "/\" ('not' x)) by WAYBEL_1:def_3
.= y "/\" ('not' x) by A6, A8, YELLOW_0:24 ;
 x "\/" y = Top L by A5, WAYBEL_1:def_23;
then  'not' x = (x "\/" y) "/\" ('not' x) by A7, YELLOW_0:25
.= (x "/\" ('not' x)) "\/" (y "/\" ('not' x)) by WAYBEL_1:def_3
.= y "/\" ('not' x) by A3, A8, YELLOW_0:24 ;
hence  y = 'not' x by A9; ::_thesis: verum
end;
thus  ( y = 'not' x implies y is_a_complement_of x ) by A1, WAYBEL_1:86; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
funca \ b ->  Element of L equals :: YELLOW_5:def 1
a "/\" ('not' b);
correctness
coherence
a "/\" ('not' b) is Element of L;
;
end;

:: deftheorem  defines \ YELLOW_5:def_1_:_
 for L being non empty RelStr
for a, b being Element of L holds a \ b = a "/\" ('not' b);

definition
let L be non empty RelStr ;
let a, b be Element of L;
funca \+\ b ->  Element of L equals :: YELLOW_5:def 2
(a \ b) "\/" (b \ a);
correctness
coherence
(a \ b) "\/" (b \ a) is Element of L;
;
end;

:: deftheorem  defines \+\ YELLOW_5:def_2_:_
 for L being non empty RelStr
for a, b being Element of L holds a \+\ b = (a \ b) "\/" (b \ a);

definition
let L be antisymmetric with_suprema with_infima RelStr ;
let a, b be Element of L;
:: original: \+\
redefine funca \+\ b ->  Element of L;
commutativity
 for a, b being Element of L holds a \+\ b = b \+\ a
proof
let a, b be Element of L; ::_thesis: a \+\ b = b \+\ a
thus a \+\ b = (a \ b) "\/" (b \ a)
.= b \+\ a ; ::_thesis: verum
end;
end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
preda meets b means :Def3: :: YELLOW_5:def 3
a "/\" b <> Bottom L;
end;

:: deftheorem Def3 defines meets YELLOW_5:def_3_:_
 for L being non empty RelStr
for a, b being Element of L holds
( a meets b iff a "/\" b <> Bottom L );

notation
let L be non empty RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;
end;

notation
let L be antisymmetric with_infima RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;
end;

definition
let L be antisymmetric with_infima RelStr ;
let a, b be Element of L;
:: original: meets
redefine preda meets b;
symmetry
 for a, b being Element of L st (L,b1,b2) holds
(L,b2,b1)
proof
let a, b be Element of L; ::_thesis: ( (L,a,b) implies (L,b,a) )
 ( a "/\" b <> Bottom L implies b "/\" a <> Bottom L ) ;
hence  ( (L,a,b) implies (L,b,a) ) by Def3; ::_thesis: verum
end;
end;

theorem :: YELLOW_5:12
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L st a <= c holds
a \ b <= c
proof
let L be transitive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for a, b, c being Element of L st a <= c holds
a \ b <= c
let a, b, c be Element of L; ::_thesis: ( a <= c implies a \ b <= c )
A1: a "/\" ('not' b) <= a by YELLOW_0:23;
assume  a <= c ; ::_thesis: a \ b <= c
hence  a \ b <= c by A1, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_5:13
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L st a <= b holds
a \ c <= b \ c by Th6;

theorem :: YELLOW_5:14
for L being LATTICE
for a, b, c being Element of L st a \ b <= c & b \ a <= c holds
a \+\ b <= c by Th9;

theorem :: YELLOW_5:15
for L being LATTICE
for a being Element of L holds
( a meets a iff a <> Bottom L )
proof
let L be LATTICE; ::_thesis: for a being Element of L holds
( a meets a iff a <> Bottom L )
let a be Element of L; ::_thesis: ( a meets a iff a <> Bottom L )
thus  ( a meets a implies a <> Bottom L ) ::_thesis: ( a <> Bottom L implies a meets a )
proof
assume  a meets a ; ::_thesis: a <> Bottom L
then  a "/\" a <> Bottom L by Def3;
hence  a <> Bottom L by Th2; ::_thesis: verum
end;
thus  ( a <> Bottom L implies a meets a ) ::_thesis: verum
proof
assume  a <> Bottom L ; ::_thesis: a meets a
then  a "/\" a <> Bottom L by Th2;
hence  a meets a by Def3; ::_thesis: verum
end;
end;

theorem :: YELLOW_5:16
for L being transitive antisymmetric with_infima RelStr st L is distributive holds
for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds
a <= b "\/" c
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: ( L is distributive implies for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds
a <= b "\/" c )
assume A1: L is distributive ; ::_thesis: for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds
a <= b "\/" c
let a, b, c be Element of L; ::_thesis: ( (a "/\" b) "\/" (a "/\" c) = a implies a <= b "\/" c )
assume  (a "/\" b) "\/" (a "/\" c) = a ; ::_thesis: a <= b "\/" c
then  (b "\/" c) "/\" a = a by A1, WAYBEL_1:def_3;
hence  a <= b "\/" c by YELLOW_0:23; ::_thesis: verum
end;

theorem Th17: :: YELLOW_5:17
for L being LATTICE st L is distributive holds
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
proof
let L be LATTICE; ::_thesis: ( L is distributive implies for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) )
assume A1: L is distributive ; ::_thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
let a, b, c be Element of L; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
(a "\/" b) "/\" (a "\/" c) = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c) by A1, WAYBEL_1:def_3
.= a "\/" ((a "\/" b) "/\" c) by LATTICE3:18
.= a "\/" ((c "/\" a) "\/" (c "/\" b)) by A1, WAYBEL_1:def_3
.= (a "\/" (c "/\" a)) "\/" (c "/\" b) by LATTICE3:14
.= a "\/" (c "/\" b) by LATTICE3:17 ;
hence  a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ; ::_thesis: verum
end;

theorem :: YELLOW_5:18
for L being LATTICE st L is distributive holds
for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)
proof
let L be non empty reflexive transitive antisymmetric with_suprema with_infima RelStr ; ::_thesis: ( L is distributive implies for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c) )
assume A1: L is distributive ; ::_thesis: for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)
let a, b, c be Element of L; ::_thesis: (a "\/" b) \ c = (a \ c) "\/" (b \ c)
thus (a "\/" b) \ c = (a "\/" b) "/\" ('not' c)
.= (('not' c) "/\" a) "\/" (('not' c) "/\" b) by A1, WAYBEL_1:def_3
.= (a \ c) "\/" (b \ c) ; ::_thesis: verum
end;

begin

theorem Th19: :: YELLOW_5:19
for L being non empty antisymmetric lower-bounded RelStr
for a being Element of L st a <= Bottom L holds
a = Bottom L
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for a being Element of L st a <= Bottom L holds
a = Bottom L
let a be Element of L; ::_thesis: ( a <= Bottom L implies a = Bottom L )
A1: Bottom L <= a by YELLOW_0:44;
assume  a <= Bottom L ; ::_thesis: a = Bottom L
hence  a = Bottom L by A1, YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: YELLOW_5:20
for L being lower-bounded Semilattice
for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds
a = Bottom L
proof
let L be lower-bounded Semilattice; ::_thesis: for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds
a = Bottom L
let a, b, c be Element of L; ::_thesis: ( a <= b & a <= c & b "/\" c = Bottom L implies a = Bottom L )
assume that
A1: a <= b and
A2: a <= c and
A3: b "/\" c = Bottom L ; ::_thesis: a = Bottom L
 a "/\" c <= b "/\" c by A1, Th6;
then  a <= b "/\" c by A2, Th10;
hence  a = Bottom L by A3, Th19; ::_thesis: verum
end;

theorem :: YELLOW_5:21
for L being antisymmetric with_suprema lower-bounded RelStr
for a, b being Element of L st a "\/" b = Bottom L holds
( a = Bottom L & b = Bottom L )
proof
let L be antisymmetric with_suprema lower-bounded RelStr ; ::_thesis: for a, b being Element of L st a "\/" b = Bottom L holds
( a = Bottom L & b = Bottom L )
let a, b be Element of L; ::_thesis: ( a "\/" b = Bottom L implies ( a = Bottom L & b = Bottom L ) )
assume  a "\/" b = Bottom L ; ::_thesis: ( a = Bottom L & b = Bottom L )
then  ( a <= Bottom L & b <= Bottom L ) by YELLOW_0:22;
hence  ( a = Bottom L & b = Bottom L ) by Th19; ::_thesis: verum
end;

theorem :: YELLOW_5:22
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds
a "/\" c = Bottom L
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds
a "/\" c = Bottom L
let a, b, c be Element of L; ::_thesis: ( a <= b & b "/\" c = Bottom L implies a "/\" c = Bottom L )
assume  ( a <= b & b "/\" c = Bottom L ) ; ::_thesis: a "/\" c = Bottom L
then A1: a "/\" c <= Bottom L by Th6;
 Bottom L <= a "/\" c by YELLOW_0:44;
hence  a "/\" c = Bottom L by A1, YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: YELLOW_5:23
for L being lower-bounded Semilattice
for a being Element of L holds (Bottom L) \ a = Bottom L
proof
let L be lower-bounded Semilattice; ::_thesis: for a being Element of L holds (Bottom L) \ a = Bottom L
let a be Element of L; ::_thesis: (Bottom L) \ a = Bottom L
thus (Bottom L) \ a = (Bottom L) "/\" ('not' a)
.= Bottom L by Th10, YELLOW_0:44 ; ::_thesis: verum
end;

theorem :: YELLOW_5:24
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b & b <= c holds
a meets c
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a meets b & b <= c holds
a meets c
let a, b, c be Element of L; ::_thesis: ( a meets b & b <= c implies a meets c )
assume A1: a meets b ; ::_thesis: ( not b <= c or a meets c )
A2: Bottom L <= a "/\" b by YELLOW_0:44;
assume  b <= c ; ::_thesis: a meets c
then A3: a "/\" b <= a "/\" c by Th6;
assume  not a meets c ; ::_thesis: contradiction
then  not a "/\" c <> Bottom L by Def3;
then  a "/\" b = Bottom L by A3, A2, YELLOW_0:def_3;
hence  contradiction by A1, Def3; ::_thesis: verum
end;

theorem Th25: :: YELLOW_5:25
for L being antisymmetric with_infima lower-bounded RelStr
for a being Element of L holds a "/\" (Bottom L) = Bottom L
proof
let L be antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a being Element of L holds a "/\" (Bottom L) = Bottom L
let a be Element of L; ::_thesis: a "/\" (Bottom L) = Bottom L
 ( Bottom L <= a "/\" (Bottom L) & a "/\" (Bottom L) <= Bottom L ) by YELLOW_0:23, YELLOW_0:44;
hence  a "/\" (Bottom L) = Bottom L by YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: YELLOW_5:26
for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b "/\" c holds
a meets b
proof
let L be transitive antisymmetric with_suprema with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a meets b "/\" c holds
a meets b
let a, b, c be Element of L; ::_thesis: ( a meets b "/\" c implies a meets b )
assume A1: a meets b "/\" c ; ::_thesis: a meets b
assume A2: not a meets b ; ::_thesis: contradiction
a "/\" (b "/\" c) = (a "/\" b) "/\" c by LATTICE3:16
.= (Bottom L) "/\" c by A2, Def3
.= Bottom L by Th25 ;
hence  contradiction by A1, Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:27
for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b \ c holds
a meets b
proof
let L be transitive antisymmetric with_suprema with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a meets b \ c holds
a meets b
let a, b, c be Element of L; ::_thesis: ( a meets b \ c implies a meets b )
assume A1: a meets b \ c ; ::_thesis: a meets b
assume A2: not a meets b ; ::_thesis: contradiction
a "/\" (b \ c) = (a "/\" b) "/\" ('not' c) by LATTICE3:16
.= (Bottom L) "/\" ('not' c) by A2, Def3
.= Bottom L by Th25 ;
hence  contradiction by A1, Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:28
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a being Element of L holds a misses Bottom L
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a being Element of L holds a misses Bottom L
let a be Element of L; ::_thesis: a misses Bottom L
 a "/\" (Bottom L) = Bottom L by Th25;
hence  a misses Bottom L by Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:29
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a misses c & b <= c holds
a misses b
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a misses c & b <= c holds
a misses b
let a, b, c be Element of L; ::_thesis: ( a misses c & b <= c implies a misses b )
assume that
A1: a misses c and
A2: b <= c ; ::_thesis: a misses b
 a "/\" c = Bottom L by A1, Def3;
then A3: a "/\" b <= Bottom L by A2, Th6;
 Bottom L <= a "/\" b by YELLOW_0:44;
then  a "/\" b = Bottom L by A3, YELLOW_0:def_3;
hence  a misses b by Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:30
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st ( a misses b or a misses c ) holds
a misses b "/\" c
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st ( a misses b or a misses c ) holds
a misses b "/\" c
let a, b, c be Element of L; ::_thesis: ( ( a misses b or a misses c ) implies a misses b "/\" c )
assume A1: ( a misses b or a misses c ) ; ::_thesis: a misses b "/\" c
percases ( a misses b or a misses c ) by A1;
supposeA2: a misses b ; ::_thesis: a misses b "/\" c
a "/\" (b "/\" c) = (a "/\" b) "/\" c by LATTICE3:16
.= (Bottom L) "/\" c by A2, Def3
.= Bottom L by Th25 ;
hence  a misses b "/\" c by Def3; ::_thesis: verum
end;
supposeA3: a misses c ; ::_thesis: a misses b "/\" c
a "/\" (b "/\" c) = (a "/\" c) "/\" b by LATTICE3:16
.= (Bottom L) "/\" b by A3, Def3
.= Bottom L by Th25 ;
hence  a misses b "/\" c by Def3; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW_5:31
for L being lower-bounded LATTICE
for a, b, c being Element of L st a <= b & a <= c & b misses c holds
a = Bottom L
proof
let L be lower-bounded LATTICE; ::_thesis: for a, b, c being Element of L st a <= b & a <= c & b misses c holds
a = Bottom L
let a, b, c be Element of L; ::_thesis: ( a <= b & a <= c & b misses c implies a = Bottom L )
assume that
A1: a <= b and
A2: a <= c and
A3: b misses c ; ::_thesis: a = Bottom L
 b "/\" c = Bottom L by A3, Def3;
then  ( Bottom L <= a "/\" c & a "/\" c <= Bottom L ) by A1, Th6, YELLOW_0:44;
then  a "/\" c = Bottom L by YELLOW_0:def_3;
hence  a = Bottom L by A2, Th10; ::_thesis: verum
end;

theorem :: YELLOW_5:32
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a misses b holds
a "/\" c misses b "/\" c
proof
let L be transitive antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for a, b, c being Element of L st a misses b holds
a "/\" c misses b "/\" c
let a, b, c be Element of L; ::_thesis: ( a misses b implies a "/\" c misses b "/\" c )
assume A1: a misses b ; ::_thesis: a "/\" c misses b "/\" c
(a "/\" c) "/\" (b "/\" c) = c "/\" (a "/\" (b "/\" c)) by LATTICE3:16
.= (c "/\" (a "/\" b)) "/\" c by LATTICE3:16
.= (c "/\" (Bottom L)) "/\" c by A1, Def3
.= (Bottom L) "/\" c by Th25
.= Bottom L by Th25 ;
hence  a "/\" c misses b "/\" c by Def3; ::_thesis: verum
end;

begin


theorem :: YELLOW_5:33
for L being non empty Boolean RelStr
for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)
let a, b, c be Element of L; ::_thesis: ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c))) "\/" (c "/\" a) by WAYBEL_1:5
.= ((a "\/" (b "/\" c)) "/\" b) "\/" (c "/\" a) by LATTICE3:17
.= ((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" (b "\/" (c "/\" a)) by WAYBEL_1:5
.= ((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) by WAYBEL_1:5
.= ((b "/\" c) "\/" (a "\/" (c "/\" a))) "/\" ((b "\/" c) "/\" (b "\/" a)) by LATTICE3:14
.= ((b "/\" c) "\/" a) "/\" ((b "\/" c) "/\" (b "\/" a)) by LATTICE3:17
.= ((b "\/" a) "/\" (c "\/" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) by WAYBEL_1:5
.= (b "\/" a) "/\" (((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c)) by LATTICE3:16
.= (b "\/" a) "/\" ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c))) by LATTICE3:16
.= ((b "\/" a) "/\" (b "\/" a)) "/\" ((c "\/" a) "/\" (b "\/" c)) by LATTICE3:16
.= (b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c)) by Th2
.= ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) by LATTICE3:16 ;
hence  ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ; ::_thesis: verum
end;

theorem Th34: :: YELLOW_5:34
for L being non empty Boolean RelStr
for a being Element of L holds
( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a being Element of L holds
( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
let a be Element of L; ::_thesis: ( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
 'not' a is_a_complement_of a by Th11;
hence  ( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L ) by WAYBEL_1:def_23; ::_thesis: verum
end;

theorem :: YELLOW_5:35
for L being non empty Boolean RelStr
for a, b, c being Element of L st a \ b <= c holds
a <= b "\/" c
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L st a \ b <= c holds
a <= b "\/" c
let a, b, c be Element of L; ::_thesis: ( a \ b <= c implies a <= b "\/" c )
A1: a <= a "\/" b by YELLOW_0:22;
assume  a \ b <= c ; ::_thesis: a <= b "\/" c
then A2: (a "/\" ('not' b)) "\/" b <= c "\/" b by Th7;
(a "/\" ('not' b)) "\/" b = (b "\/" a) "/\" (b "\/" ('not' b)) by Th17
.= (b "\/" a) "/\" (Top L) by Th34
.= a "\/" b by WAYBEL_1:4 ;
hence  a <= b "\/" c by A2, A1, YELLOW_0:def_2; ::_thesis: verum
end;

theorem Th36: :: YELLOW_5:36
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds
( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
let a, b be Element of L; ::_thesis: ( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
A1: (a "\/" b) "/\" (('not' a) "/\" ('not' b)) = ((a "\/" b) "/\" ('not' a)) "/\" ('not' b) by LATTICE3:16
.= ((('not' a) "/\" a) "\/" (('not' a) "/\" b)) "/\" ('not' b) by WAYBEL_1:def_3
.= ((Bottom L) "\/" (('not' a) "/\" b)) "/\" ('not' b) by Th34
.= (('not' a) "/\" b) "/\" ('not' b) by WAYBEL_1:3
.= ('not' a) "/\" (b "/\" ('not' b)) by LATTICE3:16
.= ('not' a) "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ;
(a "\/" b) "\/" (('not' a) "/\" ('not' b)) = a "\/" (b "\/" (('not' a) "/\" ('not' b))) by LATTICE3:14
.= a "\/" ((b "\/" ('not' a)) "/\" (b "\/" ('not' b))) by Th17
.= a "\/" ((b "\/" ('not' a)) "/\" (Top L)) by Th34
.= a "\/" (b "\/" ('not' a)) by WAYBEL_1:4
.= (a "\/" ('not' a)) "\/" b by LATTICE3:14
.= (Top L) "\/" b by Th34
.= Top L by WAYBEL_1:4 ;
then  ('not' a) "/\" ('not' b) is_a_complement_of a "\/" b by A1, WAYBEL_1:def_23;
hence  'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th11; ::_thesis: 'not' (a "/\" b) = ('not' a) "\/" ('not' b)
A2: (a "/\" b) "/\" (('not' a) "\/" ('not' b)) = a "/\" (b "/\" (('not' a) "\/" ('not' b))) by LATTICE3:16
.= a "/\" ((b "/\" ('not' a)) "\/" (b "/\" ('not' b))) by WAYBEL_1:def_3
.= a "/\" ((b "/\" ('not' a)) "\/" (Bottom L)) by Th34
.= a "/\" (b "/\" ('not' a)) by WAYBEL_1:3
.= (a "/\" ('not' a)) "/\" b by LATTICE3:16
.= (Bottom L) "/\" b by Th34
.= Bottom L by WAYBEL_1:3 ;
(a "/\" b) "\/" (('not' a) "\/" ('not' b)) = ((a "/\" b) "\/" ('not' a)) "\/" ('not' b) by LATTICE3:14
.= ((('not' a) "\/" a) "/\" (('not' a) "\/" b)) "\/" ('not' b) by Th17
.= ((Top L) "/\" (('not' a) "\/" b)) "\/" ('not' b) by Th34
.= (('not' a) "\/" b) "\/" ('not' b) by WAYBEL_1:4
.= ('not' a) "\/" (b "\/" ('not' b)) by LATTICE3:14
.= ('not' a) "\/" (Top L) by Th34
.= Top L by WAYBEL_1:4 ;
then  ('not' a) "\/" ('not' b) is_a_complement_of a "/\" b by A2, WAYBEL_1:def_23;
hence  'not' (a "/\" b) = ('not' a) "\/" ('not' b) by Th11; ::_thesis: verum
end;

theorem Th37: :: YELLOW_5:37
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
'not' b <= 'not' a
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L st a <= b holds
'not' b <= 'not' a
let a, b be Element of L; ::_thesis: ( a <= b implies 'not' b <= 'not' a )
assume  a <= b ; ::_thesis: 'not' b <= 'not' a
then  'not' a = 'not' (b "/\" a) by Th10
.= ('not' b) "\/" ('not' a) by Th36 ;
hence  'not' b <= 'not' a by YELLOW_0:22; ::_thesis: verum
end;

theorem :: YELLOW_5:38
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b holds
c \ b <= c \ a
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L st a <= b holds
c \ b <= c \ a
let a, b, c be Element of L; ::_thesis: ( a <= b implies c \ b <= c \ a )
assume  a <= b ; ::_thesis: c \ b <= c \ a
then  'not' b <= 'not' a by Th37;
then  c "/\" ('not' b) <= c "/\" ('not' a) by Th6;
hence  c \ b <= c \ a ; ::_thesis: verum
end;

theorem :: YELLOW_5:39
for L being non empty Boolean RelStr
for a, b, c, d being Element of L st a <= b & c <= d holds
a \ d <= b \ c
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c, d being Element of L st a <= b & c <= d holds
a \ d <= b \ c
let a, b, c, d be Element of L; ::_thesis: ( a <= b & c <= d implies a \ d <= b \ c )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: a \ d <= b \ c
 'not' d <= 'not' c by A2, Th37;
then A3: a "/\" ('not' d) <= a "/\" ('not' c) by Th6;
 a "/\" ('not' c) <= b "/\" ('not' c) by A1, Th6;
hence  a \ d <= b \ c by A3, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_5:40
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b "\/" c holds
( a \ b <= c & a \ c <= b )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L st a <= b "\/" c holds
( a \ b <= c & a \ c <= b )
let a, b, c be Element of L; ::_thesis: ( a <= b "\/" c implies ( a \ b <= c & a \ c <= b ) )
assume A1: a <= b "\/" c ; ::_thesis: ( a \ b <= c & a \ c <= b )
(b "\/" c) "/\" ('not' b) = (('not' b) "/\" b) "\/" (('not' b) "/\" c) by WAYBEL_1:def_3
.= (Bottom L) "\/" (('not' b) "/\" c) by Th34
.= c "/\" ('not' b) by WAYBEL_1:3 ;
then  ( c "/\" ('not' b) <= c & a "/\" ('not' b) <= c "/\" ('not' b) ) by A1, Th6, YELLOW_0:23;
hence  a \ b <= c by YELLOW_0:def_2; ::_thesis: a \ c <= b
(b "\/" c) "/\" ('not' c) = (('not' c) "/\" b) "\/" (('not' c) "/\" c) by WAYBEL_1:def_3
.= (('not' c) "/\" b) "\/" (Bottom L) by Th34
.= ('not' c) "/\" b by WAYBEL_1:3 ;
then  ( ('not' c) "/\" b <= b & a "/\" ('not' c) <= ('not' c) "/\" b ) by A1, Th6, YELLOW_0:23;
hence  a \ c <= b by YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: YELLOW_5:41
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds
( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )
let a, b be Element of L; ::_thesis: ( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )
 ( 'not' a <= ('not' a) "\/" ('not' b) & 'not' b <= ('not' a) "\/" ('not' b) ) by YELLOW_0:22;
hence  ( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) ) by Th36; ::_thesis: verum
end;

theorem :: YELLOW_5:42
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds
( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
let a, b be Element of L; ::_thesis: ( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
 ( ('not' a) "/\" ('not' b) <= 'not' a & ('not' a) "/\" ('not' b) <= 'not' b ) by YELLOW_0:23;
hence  ( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b ) by Th36; ::_thesis: verum
end;

theorem :: YELLOW_5:43
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b \ a holds
a = Bottom L
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L st a <= b \ a holds
a = Bottom L
let a, b be Element of L; ::_thesis: ( a <= b \ a implies a = Bottom L )
assume A1: a <= b \ a ; ::_thesis: a = Bottom L
(b "/\" ('not' a)) "/\" a = b "/\" (('not' a) "/\" a) by LATTICE3:16
.= b "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ;
hence  a = Bottom L by A1, Th10; ::_thesis: verum
end;

theorem :: YELLOW_5:44
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
b = a "\/" (b \ a)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L st a <= b holds
b = a "\/" (b \ a)
let a, b be Element of L; ::_thesis: ( a <= b implies b = a "\/" (b \ a) )
assume A1: a <= b ; ::_thesis: b = a "\/" (b \ a)
a "\/" (b \ a) = (a "\/" b) "/\" (a "\/" ('not' a)) by WAYBEL_1:5
.= b "/\" (('not' a) "\/" a) by A1, Th8
.= b "/\" (Top L) by Th34
.= b by WAYBEL_1:4 ;
hence  b = a "\/" (b \ a) ; ::_thesis: verum
end;

theorem :: YELLOW_5:45
for L being non empty Boolean RelStr
for a, b being Element of L holds
( a \ b = Bottom L iff a <= b )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds
( a \ b = Bottom L iff a <= b )
let a, b be Element of L; ::_thesis: ( a \ b = Bottom L iff a <= b )
thus  ( a \ b = Bottom L implies a <= b ) ::_thesis: ( a <= b implies a \ b = Bottom L )
proof
assume  a \ b = Bottom L ; ::_thesis: a <= b
then  (b "\/" a) "/\" (b "\/" ('not' b)) <= b "\/" (Bottom L) by Th17;
then  (b "\/" a) "/\" (b "\/" ('not' b)) <= b by WAYBEL_1:3;
then  (a "\/" b) "/\" (Top L) <= b by Th34;
then A1: a "\/" b <= b by WAYBEL_1:4;
 a <= a "\/" b by YELLOW_0:22;
hence  a <= b by A1, YELLOW_0:def_2; ::_thesis: verum
end;
thus  ( a <= b implies a \ b = Bottom L ) ::_thesis: verum
proof
assume  a <= b ; ::_thesis: a \ b = Bottom L
then  a "/\" ('not' b) <= b "/\" ('not' b) by Th6;
then A2: a "/\" ('not' b) <= Bottom L by Th34;
 Bottom L <= a \ b by YELLOW_0:44;
hence  a \ b = Bottom L by A2, YELLOW_0:def_3; ::_thesis: verum
end;
end;

theorem :: YELLOW_5:46
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds
a <= b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds
a <= b
let a, b, c be Element of L; ::_thesis: ( a <= b "\/" c & a "/\" c = Bottom L implies a <= b )
assume  ( a <= b "\/" c & a "/\" c = Bottom L ) ; ::_thesis: a <= b
then  ( a "/\" (b "\/" c) = a & a "/\" (b "\/" c) = (a "/\" b) "\/" (Bottom L) ) by Th10, WAYBEL_1:def_3;
then  a "/\" b = a by WAYBEL_1:3;
hence  a <= b by YELLOW_0:23; ::_thesis: verum
end;

theorem :: YELLOW_5:47
for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" b = (a \ b) "\/" b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a "\/" b = (a \ b) "\/" b
let a, b be Element of L; ::_thesis: a "\/" b = (a \ b) "\/" b
thus (a \ b) "\/" b = (b "\/" a) "/\" (b "\/" ('not' b)) by Th17
.= (b "\/" a) "/\" (Top L) by Th34
.= a "\/" b by WAYBEL_1:4 ; ::_thesis: verum
end;

theorem :: YELLOW_5:48
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "\/" b) = Bottom L
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a \ (a "\/" b) = Bottom L
let a, b be Element of L; ::_thesis: a \ (a "\/" b) = Bottom L
thus a \ (a "\/" b) = a "/\" (('not' a) "/\" ('not' b)) by Th36
.= (a "/\" ('not' a)) "/\" ('not' b) by LATTICE3:16
.= (Bottom L) "/\" ('not' b) by Th34
.= Bottom L by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:49
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "/\" b) = a \ b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a \ (a "/\" b) = a \ b
let a, b be Element of L; ::_thesis: a \ (a "/\" b) = a \ b
thus a \ (a "/\" b) = a "/\" (('not' a) "\/" ('not' b)) by Th36
.= (a "/\" ('not' a)) "\/" (a "/\" ('not' b)) by WAYBEL_1:def_3
.= (Bottom L) "\/" (a "/\" ('not' b)) by Th34
.= a \ b by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:50
for L being non empty Boolean RelStr
for a, b being Element of L holds (a \ b) "/\" b = Bottom L
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds (a \ b) "/\" b = Bottom L
let a, b be Element of L; ::_thesis: (a \ b) "/\" b = Bottom L
thus (a \ b) "/\" b = a "/\" (('not' b) "/\" b) by LATTICE3:16
.= a "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:51
for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" (b \ a) = a "\/" b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a "\/" (b \ a) = a "\/" b
let a, b be Element of L; ::_thesis: a "\/" (b \ a) = a "\/" b
thus a "\/" (b \ a) = (a "\/" b) "/\" (a "\/" ('not' a)) by Th17
.= (a "\/" b) "/\" (Top L) by Th34
.= a "\/" b by WAYBEL_1:4 ; ::_thesis: verum
end;

theorem :: YELLOW_5:52
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "/\" b) "\/" (a \ b) = a
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds (a "/\" b) "\/" (a \ b) = a
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" (a \ b) = a
thus (a "/\" b) "\/" (a \ b) = ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" ('not' b)) by Th17
.= a "/\" ((a "/\" b) "\/" ('not' b)) by LATTICE3:17
.= a "/\" ((('not' b) "\/" a) "/\" (('not' b) "\/" b)) by Th17
.= a "/\" ((('not' b) "\/" a) "/\" (Top L)) by Th34
.= a "/\" (('not' b) "\/" a) by WAYBEL_1:4
.= a by LATTICE3:18 ; ::_thesis: verum
end;

theorem :: YELLOW_5:53
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b \ c) = (a \ b) "\/" (a "/\" c)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds a \ (b \ c) = (a \ b) "\/" (a "/\" c)
let a, b, c be Element of L; ::_thesis: a \ (b \ c) = (a \ b) "\/" (a "/\" c)
thus a \ (b \ c) = a "/\" (('not' b) "\/" ('not' ('not' c))) by Th36
.= a "/\" (('not' b) "\/" c) by WAYBEL_1:87
.= (a \ b) "\/" (a "/\" c) by WAYBEL_1:def_3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:54
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a \ b) = a "/\" b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a \ (a \ b) = a "/\" b
let a, b be Element of L; ::_thesis: a \ (a \ b) = a "/\" b
thus a \ (a \ b) = a "/\" (('not' a) "\/" ('not' ('not' b))) by Th36
.= a "/\" (('not' a) "\/" b) by WAYBEL_1:87
.= (a "/\" ('not' a)) "\/" (a "/\" b) by WAYBEL_1:def_3
.= (Bottom L) "\/" (a "/\" b) by Th34
.= a "/\" b by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:55
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "\/" b) \ b = a \ b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds (a "\/" b) \ b = a \ b
let a, b be Element of L; ::_thesis: (a "\/" b) \ b = a \ b
thus (a "\/" b) \ b = (a "\/" b) "/\" ('not' b)
.= (a "/\" ('not' b)) "\/" (b "/\" ('not' b)) by WAYBEL_1:def_3
.= (a "/\" ('not' b)) "\/" (Bottom L) by Th34
.= a \ b by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:56
for L being non empty Boolean RelStr
for a, b being Element of L holds
( a "/\" b = Bottom L iff a \ b = a )
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds
( a "/\" b = Bottom L iff a \ b = a )
let a, b be Element of L; ::_thesis: ( a "/\" b = Bottom L iff a \ b = a )
thus  ( a "/\" b = Bottom L implies a \ b = a ) ::_thesis: ( a \ b = a implies a "/\" b = Bottom L )
proof
assume  a "/\" b = Bottom L ; ::_thesis: a \ b = a
then  a <= 'not' b by WAYBEL_1:82;
then  a "/\" a <= a "/\" ('not' b) by Th6;
then A1: a <= a "/\" ('not' b) by Th2;
 a \ b <= a by YELLOW_0:23;
hence  a \ b = a by A1, YELLOW_0:def_3; ::_thesis: verum
end;
thus  ( a \ b = a implies a "/\" b = Bottom L ) ::_thesis: verum
proof
assume  a \ b = a ; ::_thesis: a "/\" b = Bottom L
then  ('not' a) "\/" ('not' ('not' b)) = 'not' a by Th36;
then  a "/\" (('not' a) "\/" b) <= a "/\" ('not' a) by WAYBEL_1:87;
then  (a "/\" ('not' a)) "\/" (a "/\" b) <= a "/\" ('not' a) by WAYBEL_1:def_3;
then  (Bottom L) "\/" (a "/\" b) <= a "/\" ('not' a) by Th34;
then  (Bottom L) "\/" (a "/\" b) <= Bottom L by Th34;
then A2: a "/\" b <= Bottom L by WAYBEL_1:3;
 Bottom L <= a "/\" b by YELLOW_0:44;
hence  a "/\" b = Bottom L by A2, YELLOW_0:def_3; ::_thesis: verum
end;
end;

theorem :: YELLOW_5:57
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b "\/" c) = (a \ b) "/\" (a \ c)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds a \ (b "\/" c) = (a \ b) "/\" (a \ c)
let a, b, c be Element of L; ::_thesis: a \ (b "\/" c) = (a \ b) "/\" (a \ c)
thus a \ (b "\/" c) = a "/\" (('not' b) "/\" ('not' c)) by Th36
.= (a "/\" a) "/\" (('not' b) "/\" ('not' c)) by Th2
.= ((a "/\" a) "/\" ('not' b)) "/\" ('not' c) by LATTICE3:16
.= (a "/\" (a "/\" ('not' b))) "/\" ('not' c) by LATTICE3:16
.= (a \ b) "/\" (a \ c) by LATTICE3:16 ; ::_thesis: verum
end;

theorem :: YELLOW_5:58
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)
let a, b, c be Element of L; ::_thesis: a \ (b "/\" c) = (a \ b) "\/" (a \ c)
thus a \ (b "/\" c) = a "/\" (('not' b) "\/" ('not' c)) by Th36
.= (a \ b) "\/" (a \ c) by WAYBEL_1:def_3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:59
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)
let a, b, c be Element of L; ::_thesis: a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)
thus (a "/\" b) \ (a "/\" c) = (a "/\" b) "/\" (('not' a) "\/" ('not' c)) by Th36
.= ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' c)) by WAYBEL_1:def_3
.= ((a "/\" ('not' a)) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) by LATTICE3:16
.= ((Bottom L) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) by Th34
.= (Bottom L) "\/" ((a "/\" b) "/\" ('not' c)) by WAYBEL_1:3
.= (a "/\" b) "/\" ('not' c) by WAYBEL_1:3
.= a "/\" (b \ c) by LATTICE3:16 ; ::_thesis: verum
end;

theorem :: YELLOW_5:60
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
let a, b be Element of L; ::_thesis: (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
thus (a "\/" b) \ (a "/\" b) = (a "\/" b) "/\" (('not' a) "\/" ('not' b)) by Th36
.= ((a "\/" b) "/\" ('not' a)) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:def_3
.= ((a "/\" ('not' a)) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:def_3
.= ((Bottom L) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) by Th34
.= (b \ a) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:3
.= (b \ a) "\/" ((a "/\" ('not' b)) "\/" (b "/\" ('not' b))) by WAYBEL_1:def_3
.= (b \ a) "\/" ((a "/\" ('not' b)) "\/" (Bottom L)) by Th34
.= (a \ b) "\/" (b \ a) by WAYBEL_1:3 ; ::_thesis: verum
end;

theorem :: YELLOW_5:61
for L being non empty Boolean RelStr
for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)
let a, b, c be Element of L; ::_thesis: (a \ b) \ c = a \ (b "\/" c)
thus (a \ b) \ c = a "/\" (('not' b) "/\" ('not' c)) by LATTICE3:16
.= a \ (b "\/" c) by Th36 ; ::_thesis: verum
end;

theorem Th62: :: YELLOW_5:62
for L being non empty Boolean RelStr holds 'not' (Bottom L) = Top L
proof
let L be non empty Boolean RelStr ; ::_thesis: 'not' (Bottom L) = Top L
 ( (Bottom L) "/\" (Top L) = Bottom L & (Bottom L) "\/" (Top L) = Top L ) by WAYBEL_1:3;
then  Top L is_a_complement_of Bottom L by WAYBEL_1:def_23;
hence  'not' (Bottom L) = Top L by Th11; ::_thesis: verum
end;

theorem :: YELLOW_5:63
for L being non empty Boolean RelStr holds 'not' (Top L) = Bottom L
proof
let L be non empty Boolean RelStr ; ::_thesis: 'not' (Top L) = Bottom L
 ( (Bottom L) "/\" (Top L) = Bottom L & (Bottom L) "\/" (Top L) = Top L ) by WAYBEL_1:3;
then  Bottom L is_a_complement_of Top L by WAYBEL_1:def_23;
hence  'not' (Top L) = Bottom L by Th11; ::_thesis: verum
end;

theorem :: YELLOW_5:64
for L being non empty Boolean RelStr
for a being Element of L holds a \ a = Bottom L by Th34;

theorem :: YELLOW_5:65
for L being non empty Boolean RelStr
for a being Element of L holds a \ (Bottom L) = a
proof
let L be non empty Boolean RelStr ; ::_thesis: for a being Element of L holds a \ (Bottom L) = a
let a be Element of L; ::_thesis: a \ (Bottom L) = a
thus a \ (Bottom L) = a "/\" (Top L) by Th62
.= a by WAYBEL_1:4 ; ::_thesis: verum
end;

theorem :: YELLOW_5:66
for L being non empty Boolean RelStr
for a, b being Element of L holds 'not' (a \ b) = ('not' a) "\/" b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds 'not' (a \ b) = ('not' a) "\/" b
let a, b be Element of L; ::_thesis: 'not' (a \ b) = ('not' a) "\/" b
thus  'not' (a \ b) = ('not' a) "\/" ('not' ('not' b)) by Th36
.= ('not' a) "\/" b by WAYBEL_1:87 ; ::_thesis: verum
end;

theorem :: YELLOW_5:67
for L being non empty Boolean RelStr
for a, b being Element of L holds a "/\" b misses a \ b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a "/\" b misses a \ b
let a, b be Element of L; ::_thesis: a "/\" b misses a \ b
(a "/\" b) "/\" (a \ b) = ((a "/\" b) "/\" ('not' b)) "/\" a by LATTICE3:16
.= (a "/\" (b "/\" ('not' b))) "/\" a by LATTICE3:16
.= (a "/\" (Bottom L)) "/\" a by Th34
.= (Bottom L) "/\" a by WAYBEL_1:3
.= Bottom L by WAYBEL_1:3 ;
hence  a "/\" b misses a \ b by Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:68
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ b misses b
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L holds a \ b misses b
let a, b be Element of L; ::_thesis: a \ b misses b
(a \ b) "/\" b = a "/\" (('not' b) "/\" b) by LATTICE3:16
.= a "/\" (Bottom L) by Th34
.= Bottom L by WAYBEL_1:3 ;
hence  a \ b misses b by Def3; ::_thesis: verum
end;

theorem :: YELLOW_5:69
for L being non empty Boolean RelStr
for a, b being Element of L st a misses b holds
(a "\/" b) \ b = a
proof
let L be non empty Boolean RelStr ; ::_thesis: for a, b being Element of L st a misses b holds
(a "\/" b) \ b = a
let a, b be Element of L; ::_thesis: ( a misses b implies (a "\/" b) \ b = a )
assume  a misses b ; ::_thesis: (a "\/" b) \ b = a
then  a "/\" b = Bottom L by Def3;
then  (a "\/" ('not' b)) "/\" (b "\/" ('not' b)) <= (Bottom L) "\/" ('not' b) by Th17;
then  (a "\/" ('not' b)) "/\" (b "\/" ('not' b)) <= 'not' b by WAYBEL_1:3;
then  (a "\/" ('not' b)) "/\" (Top L) <= 'not' b by Th34;
then A1: a "\/" ('not' b) <= 'not' b by WAYBEL_1:4;
 'not' b <= a "\/" ('not' b) by YELLOW_0:22;
then  a "\/" ('not' b) = 'not' b by A1, YELLOW_0:def_3;
then A2: a <= 'not' b by YELLOW_0:22;
(a "\/" b) \ b = (a "\/" b) "/\" ('not' b)
.= (a "/\" ('not' b)) "\/" (b "/\" ('not' b)) by WAYBEL_1:def_3
.= (a "/\" ('not' b)) "\/" (Bottom L) by Th34
.= a "/\" ('not' b) by WAYBEL_1:3
.= a by A2, Th10 ;
hence  (a "\/" b) \ b = a ; ::_thesis: verum
end;