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