:: Miscellaneous Facts about Relation Structure
:: by Agnieszka Julia Marasik
::
:: Received November 8, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_2, LATTICE3, ORDERS_2, SUBSET_1, EQREL_1, XXREAL_0,
LATTICES, XBOOLE_0, WAYBEL_0, XBOOLEAN;
notations STRUCT_0, LATTICE3, WAYBEL_0, WAYBEL_1, YELLOW_0, ORDERS_2;
constructors LATTICE3, WAYBEL_1;
registrations LATTICE3, YELLOW_0, WAYBEL_1;
theorems LATTICE3, YELLOW_0, WAYBEL_1;
begin :: Introduction
theorem
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, a be Element of L;
a <= a;
then a <= a "\/" a & a "\/" a <= a by YELLOW_0:22;
hence thesis by YELLOW_0:def 3;
end;
theorem Th2:
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, a be Element of L;
a <= a;
then a "/\" a <= a & a <= a "/\" a by YELLOW_0:23;
hence thesis by YELLOW_0:def 3;
end;
theorem
for L be transitive antisymmetric with_suprema RelStr for a,b,c being
Element of L holds a"\/"b <= c implies a <= c
proof
let L be transitive antisymmetric with_suprema RelStr;
let a,b,c be Element of L;
A1: a <= a"\/"b by YELLOW_0:22;
assume a"\/"b <= c;
hence thesis by A1,YELLOW_0:def 2;
end;
theorem
for L be transitive antisymmetric with_infima RelStr for a,b,c being
Element of L holds c <= a"/\"b implies c <= a
proof
let L be transitive antisymmetric with_infima RelStr;
let a,b,c be Element of L;
A1: a"/\"b <= a by YELLOW_0:23;
assume c <= a"/\"b;
hence thesis by A1,YELLOW_0:def 2;
end;
theorem
for L be antisymmetric transitive with_suprema with_infima RelStr for
a,b,c being Element of L holds a"/\"b <= a"\/"c
proof
let L be antisymmetric transitive with_suprema with_infima RelStr;
let a,b,c be Element of L;
a"/\"b <= a & a <= a"\/"c by YELLOW_0:22,23;
hence thesis by YELLOW_0:def 2;
end;
theorem Th6:
for L be antisymmetric transitive with_infima RelStr for a,b,c be
Element of L holds a <= b implies a"/\"c <= b"/\"c
proof
let L be antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
A1: a"/\"c <= a by YELLOW_0:23;
A2: a"/\"c <= c by YELLOW_0:23;
assume a <= b;
then a"/\"c <= b by A1,YELLOW_0:def 2;
hence thesis by A2,YELLOW_0:23;
end;
theorem Th7:
for L be antisymmetric transitive with_suprema RelStr for a,b,c
be Element of L holds a <= b implies a"\/"c <= b"\/"c
proof
let L be non empty antisymmetric transitive with_suprema RelStr;
let a,b,c be Element of L;
A1: b <= b "\/" c by YELLOW_0:22;
A2: c <= b "\/" c by YELLOW_0:22;
assume a <= b;
then a <= b "\/" c by A1,YELLOW_0:def 2;
hence thesis by A2,YELLOW_0:22;
end;
theorem Th8:
for L be sup-Semilattice for a,b be Element of L holds a <= b
implies a "\/" b = b
proof
let L be sup-Semilattice;
let a,b be Element of L;
A1: b <= b;
assume a <= b;
then b <= a "\/" b & a "\/" b <= b by A1,YELLOW_0:22;
hence thesis by YELLOW_0:def 3;
end;
theorem Th9:
for L be sup-Semilattice for a,b,c being Element of L holds a <=
c & b <= c implies a"\/"b <= c
proof
let L be sup-Semilattice;
let a,b,c be Element of L;
assume that
A1: a <= c and
A2: b <= c;
c "\/" b = c by A2,Th8;
hence thesis by A1,Th7;
end;
theorem Th10:
for L be Semilattice for a,b be Element of L holds b <= a implies a"/\"b = b
proof
let L be Semilattice;
let a,b be Element of L;
assume b <= a;
then b "/\" b <= a "/\" b by Th6;
then a"/\"b <= b & b <= a "/\" b by Th2,YELLOW_0:23;
hence thesis by YELLOW_0:def 3;
end;
:: Difference in Relation Structure
begin
theorem Th11:
for L being Boolean LATTICE, x,y being Element of L holds y
is_a_complement_of x iff y = 'not' x
proof
let L be Boolean LATTICE, x,y be Element of L;
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
assume
A5: y is_a_complement_of 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;
end;
thus thesis by A1,WAYBEL_1:86;
end;
definition
let L be non empty RelStr, a,b be Element of L;
func a \ b -> Element of L equals
a "/\" 'not' b;
correctness;
end;
definition
let L be non empty RelStr, a, b be Element of L;
func a \+\ b -> Element of L equals
(a \ b) "\/" (b \ a);
correctness;
end;
definition
let L be antisymmetric with_infima with_suprema RelStr, a, b be Element of L;
redefine func a \+\ b; :: redefines \+\ (YELLOW_5, definition)
commutativity
proof
let a, b be Element of L;
thus a \+\ b = (a \ b) "\/" (b \ a) .= b \+\ a;
end;
end;
definition
let L be non empty RelStr, a, b be Element of L;
pred a meets b means
a "/\" b <> Bottom L;
end;
notation
let L be non empty RelStr, a, b be Element of L;
antonym a misses b for a meets b;
end;
notation
let L be with_infima antisymmetric RelStr, a, b be Element of L;
antonym a misses b for a meets b;
end;
definition
let L be with_infima antisymmetric RelStr, a, b be Element of L;
redefine pred a meets b; :: redefines meets (YELLOW_5, definition)
symmetry
proof
let a, b be Element of L;
a"/\"b <> Bottom L implies b"/\"a <> Bottom L;
hence thesis;
end;
end;
theorem
for L be antisymmetric transitive with_infima with_suprema RelStr for
a,b,c be Element of L holds a <= c implies a \ b <= c
proof
let L be antisymmetric transitive with_infima with_suprema RelStr;
let a,b,c be Element of L;
A1: a "/\" 'not' b <= a by YELLOW_0:23;
assume a <= c;
hence thesis by A1,YELLOW_0:def 2;
end;
theorem
for L be antisymmetric transitive with_infima with_suprema RelStr for
a,b,c be Element of L holds a <= b implies a \ c <= b \ c by Th6;
theorem
for L be LATTICE for a,b,c be Element of L holds a \ b <= c & b \ a <=
c implies a \+\ b <= c by Th9;
theorem
for L be LATTICE for a be Element of L holds a meets a iff a <> Bottom L
by Th2;
theorem
for L be antisymmetric transitive with_infima RelStr st L is
distributive for a,b,c be Element of L holds (a "/\" b) "\/" (a "/\" c) = a
implies a <= b "\/" c
proof
let L be antisymmetric transitive with_infima RelStr such that
A1: L is distributive;
let a,b,c be Element of L;
assume (a "/\" b) "\/" (a "/\" c) = a;
then (b "\/" c) "/\" a = a by A1,WAYBEL_1:def 3;
hence thesis by YELLOW_0:23;
end;
theorem Th17:
for L be LATTICE st L is distributive for a,b,c be Element of L
holds a"\/"(b"/\"c) = (a"\/"b) "/\" (a"\/"c)
proof
let L be LATTICE such that
A1: L is distributive;
let a,b,c be Element of L;
(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 thesis;
end;
theorem
for L be LATTICE st L is distributive for a,b,c be Element of L holds
(a "\/" b) \ c = (a \ c) "\/" (b \ c)
proof
let L be with_suprema with_infima reflexive transitive antisymmetric non
empty RelStr such that
A1: L is distributive;
let a,b,c be Element of L;
thus (a "\/" b) \ c = (a "\/" b) "/\" 'not' c
.= ('not' c "/\" a) "\/" ('not' c"/\" b) by A1,WAYBEL_1:def 3
.= (a \ c) "\/" (b \ c);
end;
:: Lower-bound in Relation Structure
begin
theorem Th19:
for L be lower-bounded non empty antisymmetric RelStr for a be
Element of L holds a <= Bottom L implies a = Bottom L
proof
let L be lower-bounded non empty antisymmetric RelStr;
let a be Element of L;
A1: Bottom L <= a by YELLOW_0:44;
assume a <= Bottom L;
hence thesis by A1,YELLOW_0:def 3;
end;
theorem
for L be lower-bounded Semilattice for a,b,c be Element of L holds a
<= b & a <= c & b"/\"c = Bottom L implies a = Bottom L
proof
let L be lower-bounded Semilattice;
let a,b,c be Element of L;
assume that
A1: a <= b and
A2: a <= c and
A3: b"/\"c = Bottom L;
a"/\"c <= b"/\"c by A1,Th6;
then a <= b"/\"c by A2,Th10;
hence thesis by A3,Th19;
end;
theorem
for L be lower-bounded antisymmetric with_suprema RelStr for a,b be
Element of L holds a"\/"b = Bottom L implies a = Bottom L & b = Bottom L
proof
let L be lower-bounded antisymmetric with_suprema RelStr;
let a,b be Element of L;
assume a"\/"b = Bottom L;
then a <= Bottom L & b <= Bottom L by YELLOW_0:22;
hence thesis by Th19;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a <= b & b"/\"c = Bottom L implies a"/\"c = Bottom
L
proof
let L be lower-bounded antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
assume a <= b & b"/\"c = Bottom L;
then
A1: a"/\"c <= Bottom L by Th6;
Bottom L <= a"/\"c by YELLOW_0:44;
hence thesis by A1,YELLOW_0:def 3;
end;
theorem
for L be lower-bounded Semilattice for a be Element of L holds Bottom
L \ a = Bottom L
proof
let L be lower-bounded Semilattice;
let a be Element of L;
thus Bottom L \ a = Bottom L "/\" 'not' a .= Bottom L by Th10,YELLOW_0:44;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a meets b & b <= c implies a meets c
proof
let L be lower-bounded antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
assume
A1: a meets b;
A2: Bottom L <= a"/\"b by YELLOW_0:44;
assume b <= c;
then
A3: a"/\"b <= a"/\"c by Th6;
assume not a meets c;
then not a"/\"c <> Bottom L;
then a"/\"b = Bottom L by A3,A2,YELLOW_0:def 3;
hence contradiction by A1;
end;
theorem Th25:
for L be lower-bounded with_infima antisymmetric RelStr for a be
Element of L holds a"/\"Bottom L = Bottom L
proof
let L be lower-bounded with_infima antisymmetric RelStr;
let a be Element of L;
Bottom L <= a "/\" Bottom L & a"/\"Bottom L <= Bottom L by YELLOW_0:23,44;
hence thesis by YELLOW_0:def 3;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima
with_suprema RelStr for a,b,c be Element of L holds a meets b"/\"c implies a
meets b
proof
let L be lower-bounded antisymmetric transitive with_infima with_suprema
RelStr;
let a,b,c be Element of L;
assume
A1: a meets b"/\"c;
assume
A2: not a meets b;
a"/\"(b"/\"c)= (a"/\"b)"/\"c by LATTICE3:16
.= Bottom L "/\"c by A2
.= Bottom L by Th25;
hence contradiction by A1;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima
with_suprema RelStr for a,b,c be Element of L holds a meets b\c implies a meets
b
proof
let L be lower-bounded antisymmetric transitive with_infima with_suprema
RelStr;
let a,b,c be Element of L;
assume
A1: a meets b\c;
assume
A2: not a meets b;
a"/\"(b\c) = (a"/\"b)"/\"'not' c by LATTICE3:16
.= Bottom L "/\"'not' c by A2
.= Bottom L by Th25;
hence contradiction by A1;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a be Element of L holds a misses Bottom L
by Th25;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses c & b <= c implies a misses b
proof
let L be lower-bounded antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
assume that
A1: a misses c and
A2: b <= c;
a"/\"c = Bottom L by A1;
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 thesis;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses b or a misses c implies a misses b"/\"c
proof
let L be lower-bounded antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
assume
A1: a misses b or a misses c;
per cases by A1;
suppose
A2: a misses b;
a"/\" (b"/\"c) = (a"/\"b)"/\"c by LATTICE3:16
.= Bottom L "/\" c by A2
.= Bottom L by Th25;
hence thesis;
end;
suppose
A3: a misses c;
a"/\" (b"/\"c) = (a"/\"c)"/\"b by LATTICE3:16
.= Bottom L "/\" b by A3
.= Bottom L by Th25;
hence thesis;
end;
end;
theorem
for L be lower-bounded LATTICE for a,b,c be Element of L holds a <= b
& a <= c & b misses c implies a = Bottom L
proof
let L be lower-bounded LATTICE;
let a,b,c be Element of L;
assume that
A1: a <= b and
A2: a <= c and
A3: b misses c;
b"/\"c = Bottom L by A3;
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 thesis by A2,Th10;
end;
theorem
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses b implies (a"/\"c) misses (b"/\"c)
proof
let L be lower-bounded antisymmetric transitive with_infima RelStr;
let a,b,c be Element of L;
assume
A1: a misses b;
(a"/\"c)"/\"(b"/\"c) = c"/\"(a"/\"(b"/\"c)) by LATTICE3:16
.= c"/\"(a"/\"b)"/\"c by LATTICE3:16
.= c"/\"Bottom L"/\"c by A1
.= Bottom L"/\"c by Th25
.=Bottom L by Th25;
hence thesis;
end;
:: Boolean Lattice
begin
reserve L for Boolean non empty RelStr;
reserve a,b,c,d for Element of L;
theorem
(a"/\"b) "\/" (b"/\"c) "\/" (c"/\"a) = (a"\/"b) "/\" (b"\/"c) "/\" (c
"\/" a )
proof
(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 thesis;
end;
theorem Th34:
a"/\"'not' a = Bottom L & a"\/"'not' a = Top L
proof
'not' a is_a_complement_of a by Th11;
hence thesis by WAYBEL_1:def 23;
end;
theorem
a \ b <= c implies a <= b"\/"c
proof
A1: a <= a"\/" b by YELLOW_0:22;
assume 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 thesis by A2,A1,YELLOW_0:def 2;
end;
theorem Th36:
'not' (a"\/"b) = 'not' a"/\" 'not' b & 'not' (a"/\"b) = 'not' a "\/" 'not' b
proof
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;
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;
end;
theorem Th37:
a <= b implies 'not' b <= 'not' a
proof
assume a <= b;
then 'not' a = 'not' (b"/\"a) by Th10
.= 'not' b "\/" 'not' a by Th36;
hence thesis by YELLOW_0:22;
end;
theorem
a <= b implies c\b <= c\a
proof
assume a <= b;
then 'not' b <= 'not' a by Th37;
then c"/\"'not' b <= c"/\"'not' a by Th6;
hence thesis;
end;
theorem
a <= b & c <= d implies a\d <= b\c
proof
assume that
A1: a <= b and
A2: c <= d;
'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 thesis by A3,YELLOW_0:def 2;
end;
theorem
a <= b"\/"c implies a\b <= c & a\c <= b
proof
assume
A1: a <= b"\/"c;
(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;
(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 thesis by YELLOW_0:def 2;
end;
theorem
'not' a <= 'not' (a"/\"b) & 'not' b <= 'not' (a"/\"b)
proof
'not' a <= 'not' a"\/" 'not' b & 'not' b <= 'not' a"\/" 'not' b by
YELLOW_0:22;
hence thesis by Th36;
end;
theorem
'not' (a"\/"b) <= 'not' a & 'not' (a"\/"b) <= 'not' b
proof
'not' a"/\"'not' b <= 'not' a & 'not' a"/\"'not' b <= 'not' b by YELLOW_0:23;
hence thesis by Th36;
end;
theorem
a <= b\a implies a = Bottom L
proof
assume
A1: a <= b\a;
(b"/\"'not' a) "/\" a = b"/\"('not' a"/\"a) by LATTICE3:16
.= b"/\"Bottom L by Th34
.= Bottom L by WAYBEL_1:3;
hence thesis by A1,Th10;
end;
theorem
a <= b implies b = a "\/" (b\a)
proof
assume
A1: a <= b;
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 thesis;
end;
theorem
a\b = Bottom L iff a <= b
proof
thus a\b = Bottom L implies a <= b
proof
assume a\b = Bottom L;
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 thesis by A1,YELLOW_0:def 2;
end;
thus a <= b implies a\b = Bottom L
proof
assume a <= b;
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 thesis by A2,YELLOW_0:def 3;
end;
end;
theorem
a <= b"\/"c & a"/\"c = Bottom L implies a <= b
proof
assume a <= b"\/"c & a"/\"c = Bottom L;
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 thesis by YELLOW_0:23;
end;
theorem
a"\/"b = (a\b)"\/"b
proof
thus (a\b)"\/"b = (b"\/"a)"/\"(b"\/"'not' b) by Th17
.= (b"\/"a)"/\" Top L by Th34
.= a"\/"b by WAYBEL_1:4;
end;
theorem
a\(a"\/"b) = Bottom L
proof
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;
end;
theorem
a\a"/\"b = a\b
proof
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;
end;
theorem
(a\b)"/\"b = Bottom L
proof
thus (a\b)"/\"b = a"/\"('not' b"/\"b) by LATTICE3:16
.= a"/\"Bottom L by Th34
.= Bottom L by WAYBEL_1:3;
end;
theorem
a"\/"(b\a) = a"\/"b
proof
thus a"\/"(b\a) = (a"\/"b)"/\"(a"\/"'not' a) by Th17
.= (a"\/"b)"/\"Top L by Th34
.= a"\/"b by WAYBEL_1:4;
end;
theorem
(a"/\"b)"\/"(a\b) = a
proof
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;
end;
theorem
a\(b\c)= (a\b)"\/"(a"/\"c)
proof
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;
end;
theorem
a\(a\b) = a"/\"b
proof
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;
end;
theorem
(a"\/"b)\b = a\b
proof
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;
end;
theorem
a"/\"b = Bottom L iff a\b = a
proof
thus a"/\"b = Bottom L implies a\b = a
proof
assume a"/\"b = Bottom L;
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 thesis by A1,YELLOW_0:def 3;
end;
thus a\b = a implies a"/\"b = Bottom L
proof
assume a\b = a;
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 thesis by A2,YELLOW_0:def 3;
end;
end;
theorem
a\(b"\/"c) = (a\b)"/\"(a\c)
proof
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;
end;
theorem
a\(b"/\"c) = (a\b)"\/"(a\c)
proof
thus a\(b"/\"c) = a"/\"('not' b"\/"'not' c) by Th36
.= (a\b)"\/"(a\c) by WAYBEL_1:def 3;
end;
theorem
a"/\"(b\c) = a"/\"b \ a"/\"c
proof
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;
end;
theorem
(a"\/"b)\(a"/\"b) = (a\b)"\/"(b\a)
proof
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;
end;
theorem
(a\b)\c = a\(b"\/"c)
proof
thus (a\b)\c = a"/\"('not' b"/\"'not' c) by LATTICE3:16
.= a\(b"\/"c) by Th36;
end;
theorem Th62:
'not' (Bottom L) = Top L
proof
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 thesis by Th11;
end;
theorem
'not' (Top L) = Bottom L
proof
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 thesis by Th11;
end;
theorem
a\a = Bottom L by Th34;
theorem
a \ Bottom L = a
proof
thus a \ Bottom L = a"/\"Top L by Th62
.= a by WAYBEL_1:4;
end;
theorem
'not' (a\b) = 'not' a"\/"b
proof
thus 'not' (a\b) = 'not' a"\/"'not' 'not' b by Th36
.= 'not' a"\/"b by WAYBEL_1:87;
end;
theorem
a"/\"b misses a\b
proof
(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 thesis;
end;
theorem
(a\b) misses b
proof
(a\b)"/\"b = a"/\"('not' b"/\"b) by LATTICE3:16
.= a"/\"Bottom L by Th34
.= Bottom L by WAYBEL_1:3;
hence thesis;
end;
theorem
a misses b implies (a"\/"b)\b = a
proof
assume a misses b;
then a"/\"b = Bottom L;
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 thesis;
end;