environ vocabulary RELAT_2, LATTICE3, ORDERS_1, LATTICES, WAYBEL_0, ZF_LANG, BOOLE; notation STRUCT_0, LATTICE3, WAYBEL_0, WAYBEL_1, YELLOW_0, ORDERS_1; constructors WAYBEL_1, LATTICE3; clusters LATTICE3, WAYBEL_1; begin :: Introduction theorem :: YELLOW_5:1 for L being reflexive antisymmetric with_suprema RelStr for a being Element of L holds a "\/" a = a; theorem :: YELLOW_5:2 for L being reflexive antisymmetric with_infima RelStr for a being Element of L holds a "/\" a = a; theorem :: YELLOW_5:3 for L be transitive antisymmetric with_suprema RelStr for a,b,c being Element of L holds a"\/"b <= c implies a <= c; theorem :: YELLOW_5:4 for L be transitive antisymmetric with_infima RelStr for a,b,c being Element of L holds c <= a"/\"b implies c <= a; theorem :: YELLOW_5:5 for L be antisymmetric transitive with_suprema with_infima RelStr for a,b,c being Element of L holds a"/\"b <= a"\/"c; theorem :: YELLOW_5:6 for L be antisymmetric transitive with_infima RelStr for a,b,c be Element of L holds a <= b implies a"/\"c <= b"/\"c; theorem :: YELLOW_5:7 for L be antisymmetric transitive with_suprema RelStr for a,b,c be Element of L holds a <= b implies a"\/"c <= b"\/"c; theorem :: YELLOW_5:8 for L be sup-Semilattice for a,b be Element of L holds a <= b implies a "\/" b = b; theorem :: YELLOW_5:9 for L be sup-Semilattice for a,b,c being Element of L holds a <= c & b <= c implies a"\/"b <= c; theorem :: YELLOW_5:10 for L be Semilattice for a,b be Element of L holds b <= a implies a"/\"b = b; :: Difference in Relation Structure begin theorem :: YELLOW_5:11 for L being Boolean LATTICE, x,y being Element of L holds y is_a_complement_of x iff y = 'not' x; definition let L be non empty RelStr, a,b be Element of L; func a \ b -> Element of L equals :: YELLOW_5:def 1 a "/\" 'not' b; end; definition let L be non empty RelStr, a, b be Element of L; func a \+\ b -> Element of L equals :: YELLOW_5:def 2 (a \ b) "\/" (b \ a); end; definition let L be antisymmetric with_infima with_suprema RelStr, a, b be Element of L; redefine func a \+\ b; commutativity; end; definition let L be non empty RelStr, a, b be Element of L; pred a meets b means :: YELLOW_5:def 3 a "/\" b <> Bottom L; antonym a misses b; end; definition let L be with_infima antisymmetric RelStr, a, b be Element of L; redefine pred a meets b; symmetry; antonym a misses b; end; theorem :: YELLOW_5:12 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; theorem :: YELLOW_5:13 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; theorem :: YELLOW_5:14 for L be antisymmetric transitive with_infima with_suprema RelStr for a,b be Element of L holds a \ b <= a; theorem :: YELLOW_5:15 for L be antisymmetric transitive with_infima with_suprema RelStr for a,b be Element of L holds a \ b <= a \+\ b; theorem :: YELLOW_5:16 for L be LATTICE for a,b,c be Element of L holds a \ b <= c & b \ a <= c implies a \+\ b <= c; theorem :: YELLOW_5:17 for L be LATTICE for a be Element of L holds a meets a iff a <> Bottom L; theorem :: YELLOW_5:18 for L be antisymmetric transitive with_infima with_suprema RelStr for a,b,c be Element of L holds a "/\" (b \ c) = (a "/\" b) \ c; theorem :: YELLOW_5:19 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; theorem :: YELLOW_5:20 for L be LATTICE st L is distributive for a,b,c be Element of L holds a"\/"(b"/\"c) = (a"\/"b) "/\" (a"\/"c); theorem :: YELLOW_5:21 for L be LATTICE st L is distributive for a,b,c be Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c); :: Lower-bound in Relation Structure begin theorem :: YELLOW_5:22 for L be lower-bounded non empty antisymmetric RelStr for a be Element of L holds a <= Bottom L implies a = Bottom L; theorem :: YELLOW_5:23 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; theorem :: YELLOW_5:24 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; theorem :: YELLOW_5:25 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; theorem :: YELLOW_5:26 for L be lower-bounded Semilattice for a be Element of L holds Bottom L \ a = Bottom L; theorem :: YELLOW_5:27 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; theorem :: YELLOW_5:28 for L be lower-bounded with_infima antisymmetric RelStr for a be Element of L holds a"/\"Bottom L = Bottom L; theorem :: YELLOW_5:29 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; theorem :: YELLOW_5:30 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; theorem :: YELLOW_5:31 for L be lower-bounded antisymmetric transitive with_infima RelStr for a be Element of L holds a misses Bottom L; theorem :: YELLOW_5:32 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; theorem :: YELLOW_5:33 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; theorem :: YELLOW_5:34 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; theorem :: YELLOW_5:35 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); :: Boolean Lattice begin reserve L for Boolean (non empty RelStr); reserve a,b,c,d for Element of L; theorem :: YELLOW_5:36 (a"/\"b) "\/" (b"/\"c) "\/" (c"/\"a) = (a"\/"b) "/\" (b"\/"c) "/\" (c"\/"a); theorem :: YELLOW_5:37 a"/\"'not' a = Bottom L & a"\/"'not' a = Top L; theorem :: YELLOW_5:38 a \ b <= c implies a <= b"\/"c; theorem :: YELLOW_5:39 'not' (a"\/"b) = 'not' a"/\" 'not' b & 'not' (a"/\"b) = 'not' a"\/" 'not' b; theorem :: YELLOW_5:40 a <= b implies 'not' b <= 'not' a; theorem :: YELLOW_5:41 a <= b implies c\b <= c\a; theorem :: YELLOW_5:42 a <= b & c <= d implies a\d <= b\c; theorem :: YELLOW_5:43 a <= b"\/"c implies a\b <= c & a\c <= b; theorem :: YELLOW_5:44 'not' a <= 'not' (a"/\"b) & 'not' b <= 'not' (a"/\"b); theorem :: YELLOW_5:45 'not' (a"\/"b) <= 'not' a & 'not' (a"\/"b) <= 'not' b; theorem :: YELLOW_5:46 a <= b\a implies a = Bottom L; theorem :: YELLOW_5:47 a <= b implies b = a "\/" (b\a); theorem :: YELLOW_5:48 a\b = Bottom L iff a <= b; theorem :: YELLOW_5:49 (a <= b"\/"c & a"/\"c = Bottom L) implies a <= b; theorem :: YELLOW_5:50 a"\/"b = (a\b)"\/"b; theorem :: YELLOW_5:51 a\(a"\/"b) = Bottom L; theorem :: YELLOW_5:52 a\a"/\"b = a\b; theorem :: YELLOW_5:53 (a\b)"/\"b = Bottom L; theorem :: YELLOW_5:54 a"\/"(b\a) = a"\/"b; theorem :: YELLOW_5:55 (a"/\"b)"\/"(a\b) = a; theorem :: YELLOW_5:56 a\(b\c)= (a\b)"\/"(a"/\"c); theorem :: YELLOW_5:57 a\(a\b) = a"/\"b; theorem :: YELLOW_5:58 (a"\/"b)\b = a\b; theorem :: YELLOW_5:59 a"/\"b = Bottom L iff a\b = a; theorem :: YELLOW_5:60 a\(b"\/"c) = (a\b)"/\"(a\c); theorem :: YELLOW_5:61 a\(b"/\"c) = (a\b)"\/"(a\c); theorem :: YELLOW_5:62 a"/\"(b\c) = a"/\"b \ a"/\"c; theorem :: YELLOW_5:63 (a"\/"b)\(a"/\"b) = (a\b)"\/"(b\a); theorem :: YELLOW_5:64 (a\b)\c = a\(b"\/"c); theorem :: YELLOW_5:65 'not' (Bottom L) = Top L; theorem :: YELLOW_5:66 'not' (Top L) = Bottom L; theorem :: YELLOW_5:67 a\a = Bottom L; theorem :: YELLOW_5:68 a \ Bottom L = a; theorem :: YELLOW_5:69 'not' (a\b) = 'not' a"\/"b; theorem :: YELLOW_5:70 a"/\"b misses a\b; theorem :: YELLOW_5:71 (a\b) misses b; theorem :: YELLOW_5:72 a misses b implies (a"\/"b)\b = a;