:: On the Characterization of Modular and Distributive Lattices :: by Adam Naumowicz :: :: Received April 3, 1998 :: Copyright (c) 1998-2019 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 NUMBERS, CARD_1, XBOOLE_0, TARSKI, RELAT_2, LATTICE3, ORDERS_2, SUBSET_1, LATTICES, EQREL_1, XXREAL_0, WAYBEL_0, YELLOW_1, STRUCT_0, CAT_1, LATTICE5, WELLORD1, FUNCT_1, SEQM_3, YELLOW_0, RELAT_1, ORDINAL2, MEASURE5, FINSET_1, ORDERS_1, REWRITE1, YELLOW11, ZFMISC_1; notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, ORDERS_1, DOMAIN_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_1, LATTICE5, WAYBEL_0; constructors DOMAIN_1, XXREAL_0, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, ORDINAL1; requirements NUMERALS, REAL, SUBSET, BOOLE; definitions TARSKI, ZFMISC_1, YELLOW_0, WAYBEL_1, FUNCT_1, WAYBEL_0, LATTICE3, XBOOLE_0; equalities WAYBEL_0, ORDINAL1, CARD_1; expansions TARSKI, ZFMISC_1, WAYBEL_1, LATTICE3, XBOOLE_0; theorems WAYBEL_1, YELLOW_0, YELLOW_3, YELLOW_5, LATTICE3, TARSKI, FUNCT_2, WAYBEL_0, ZFMISC_1, FUNCT_1, ORDERS_2, YELLOW_1, ENUMSET1, CARD_1, FINSET_1, XBOOLE_0, XBOOLE_1, NAT_1; schemes FUNCT_2, FINSET_1, XBOOLE_0; begin reserve x for set; :: Preliminaries theorem 3 = {0,1,2} by CARD_1:51; theorem Th2: 2\1={1} proof thus 2\1 c= {1} proof let x be object; assume A1: x in 2\1; then A2: x=0 or x=1 by CARD_1:50,TARSKI:def 2; not x in {0} by A1,CARD_1:49,XBOOLE_0:def 5; hence thesis by A2,TARSKI:def 1; end; let x be object; assume x in {1}; then A3: x = 1 by TARSKI:def 1; then A4: not x in {0} by TARSKI:def 1; x in {0,1} by A3,TARSKI:def 2; hence thesis by A4,CARD_1:49,50,XBOOLE_0:def 5; end; theorem Th3: 3\1 = {1,2} proof thus 3\1 c= {1,2} proof let x be object; assume A1: x in 3\1; then A2: x=0 or x=1 or x=2 by CARD_1:51,ENUMSET1:def 1; not x in {0} by A1,CARD_1:49,XBOOLE_0:def 5; hence thesis by A2,TARSKI:def 1,def 2; end; thus {1,2} c= 3\1 proof let x be object; assume x in {1,2}; then A3: x=1 or x=2 by TARSKI:def 2; then A4: not x in {0} by TARSKI:def 1; x in {0,1,2} by A3,ENUMSET1:def 1; hence thesis by A4,CARD_1:49,51,XBOOLE_0:def 5; end; end; theorem Th4: 3\2 = {2} proof thus 3\2 c= {2} proof let x be object; assume A1: x in 3\2; then A2: x=0 or x=1 or x=2 by CARD_1:51,ENUMSET1:def 1; not x in {0,1} by A1,CARD_1:50,XBOOLE_0:def 5; hence thesis by A2,TARSKI:def 1,def 2; end; thus {2} c= 3\2 proof let x be object; assume x in {2}; then A3: x=2 by TARSKI:def 1; then A4: not x in {0,1} by TARSKI:def 2; x in {0,1,2} by A3,ENUMSET1:def 1; hence thesis by A4,CARD_1:50,51,XBOOLE_0:def 5; end; end; Lm1: 3\2 c= 3\1 proof let x be object; assume x in 3\2; then x=2 by Th4,TARSKI:def 1; hence thesis by Th3,TARSKI:def 2; end; begin:: Main part theorem Th5: for L being antisymmetric reflexive with_infima with_suprema RelStr for a,b being Element of L holds a"/\"b = b iff a"\/"b = a proof let L be antisymmetric reflexive with_infima with_suprema RelStr; let a,b be Element of L; thus a"/\"b = b implies a"\/"b = a proof assume a"/\"b = b; then b <= a by YELLOW_0:23; hence thesis by YELLOW_0:24; end; assume a"\/"b = a; then b <= a by YELLOW_0:22; hence thesis by YELLOW_0:25; end; theorem Th6: for L being LATTICE for a,b,c being Element of L holds (a"/\"b)"\/"(a"/\"c) <= a"/\"(b"\/"c) proof let L be LATTICE; let a,b,c be Element of L; A1: a <= a; c <= b"\/"c by YELLOW_0:22; then A2: a"/\"c <= a"/\"(b"\/"c) by A1,YELLOW_3:2; b <= b"\/"c by YELLOW_0:22; then a"/\"b <= a"/\"(b"\/"c) by A1,YELLOW_3:2; hence thesis by A2,YELLOW_5:9; end; theorem Th7: for L being LATTICE for a,b,c being Element of L holds a"\/"(b"/\"c) <= (a"\/"b)"/\"(a"\/"c) proof let L be LATTICE; let a,b,c be Element of L; A1: a <= a; b"/\"c <= c by YELLOW_0:23; then A2: a"\/"(b"/\"c) <= a"\/"c by A1,YELLOW_3:3; b"/\"c <= b by YELLOW_0:23; then a"\/"(b"/\"c) <= a"\/"b by A1,YELLOW_3:3; hence thesis by A2,YELLOW_0:23; end; theorem Th8: for L being LATTICE for a,b,c being Element of L holds a <= c implies a"\/"(b"/\"c) <= (a"\/"b) "/\"c proof let L be LATTICE; let a,b,c be Element of L; A1: b"/\"c <= c by YELLOW_0:23; A2: a <= a; b"/\"c <= b by YELLOW_0:23; then A3: a"\/"(b"/\"c) <= a"\/"b by A2,YELLOW_3:3; assume a <= c; then a"\/"(b"/\"c) <= c by A1,YELLOW_0:22; hence thesis by A3,YELLOW_0:23; end; definition func N_5 -> RelStr equals InclPoset {0, 3 \ 1, 2, 3 \ 2, 3}; correctness; end; registration cluster N_5 -> strict reflexive transitive antisymmetric; correctness; cluster N_5 -> with_infima with_suprema; correctness proof set Z = {0, 3 \ 1, 2, 3 \ 2, 3}; set N = InclPoset Z; A1: N is with_infima proof let x,y be Element of N; A2: Z = the carrier of N by YELLOW_1:1; thus ex z being Element of N st z <= x & z <= y & for z9 being Element of N st z9 <= x & z9 <= y holds z9 <= z proof per cases by A2,ENUMSET1:def 3; suppose x = 0 & y = 0; then reconsider z = x /\ y as Element of N; take z; A3: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A3,YELLOW_1:3; let w be Element of N; assume that A4: w <= x and A5: w <= y; A6: w c= y by A5,YELLOW_1:3; w c= x by A4,YELLOW_1:3; then w c= x /\ y by A6,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 0 & y = 3\1; then reconsider z = x /\ y as Element of N; take z; A7: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A7,YELLOW_1:3; let w be Element of N; assume that A8: w <= x and A9: w <= y; A10: w c= y by A9,YELLOW_1:3; w c= x by A8,YELLOW_1:3; then w c= x /\ y by A10,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 0 & y = 2; then reconsider z = x /\ y as Element of N; take z; A11: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A11,YELLOW_1:3; let w be Element of N; assume that A12: w <= x and A13: w <= y; A14: w c= y by A13,YELLOW_1:3; w c= x by A12,YELLOW_1:3; then w c= x /\ y by A14,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 0 & y = 3\2; then reconsider z = x /\ y as Element of N; take z; A15: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A15,YELLOW_1:3; let w be Element of N; assume that A16: w <= x and A17: w <= y; A18: w c= y by A17,YELLOW_1:3; w c= x by A16,YELLOW_1:3; then w c= x /\ y by A18,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 0 & y = 3; then reconsider z = x /\ y as Element of N; take z; A19: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A19,YELLOW_1:3; let w be Element of N; assume that A20: w <= x and A21: w <= y; A22: w c= y by A21,YELLOW_1:3; w c= x by A20,YELLOW_1:3; then w c= x /\ y by A22,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3\1 & y = 0; then reconsider z = x /\ y as Element of N; take z; A23: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A23,YELLOW_1:3; let w be Element of N; assume that A24: w <= x and A25: w <= y; A26: w c= y by A25,YELLOW_1:3; w c= x by A24,YELLOW_1:3; then w c= x /\ y by A26,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3\1 & y = 3\1; then reconsider z = x /\ y as Element of N; take z; A27: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A27,YELLOW_1:3; let w be Element of N; assume that A28: w <= x and A29: w <= y; A30: w c= y by A29,YELLOW_1:3; w c= x by A28,YELLOW_1:3; then w c= x /\ y by A30,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A31: x = 3\1 & y = 2; 0 in Z by ENUMSET1:def 3; then reconsider z = 0 as Element of N by YELLOW_1:1; take z; A32: z c= y; z c= x; hence z <= x & z <= y by A32,YELLOW_1:3; let z9 be Element of N; assume that A33: z9 <= x and A34: z9 <= y; A35: z9 c= 3\1 by A31,A33,YELLOW_1:3; A36: now assume z9= 2; then 0 in z9 by CARD_1:50,TARSKI:def 2; hence contradiction by A35,Th3,TARSKI:def 2; end; A37: z9 c= 2 by A31,A34,YELLOW_1:3; A38: now assume z9= 3; then A39: 2 in z9 by CARD_1:51,ENUMSET1:def 1; not 2 in 2; hence contradiction by A37,A39; end; A40: now assume z9= 3\2; then A41: 2 in z9 by Th4,TARSKI:def 1; not 2 in 2; hence contradiction by A37,A41; end; A42: now assume z9= 3\1; then A43: 2 in z9 by Th3,TARSKI:def 2; not 2 in 2; hence contradiction by A37,A43; end; z9 is Element of Z by YELLOW_1:1; hence thesis by A42,A36,A40,A38,ENUMSET1:def 3; end; suppose x = 3\1 & y = 3\2; then reconsider z = x /\ y as Element of N by Th3,Th4,ZFMISC_1:13; take z; A44: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A44,YELLOW_1:3; let w be Element of N; assume that A45: w <= x and A46: w <= y; A47: w c= y by A46,YELLOW_1:3; w c= x by A45,YELLOW_1:3; then w c= x /\ y by A47,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A48: x = 3\1 & y = 3; (3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49 .= 3\1; then reconsider z = x /\ y as Element of N by A48; take z; A49: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A49,YELLOW_1:3; let w be Element of N; assume that A50: w <= x and A51: w <= y; A52: w c= y by A51,YELLOW_1:3; w c= x by A50,YELLOW_1:3; then w c= x /\ y by A52,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 2 & y = 0; then reconsider z = x /\ y as Element of N; take z; A53: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A53,YELLOW_1:3; let w be Element of N; assume that A54: w <= x and A55: w <= y; A56: w c= y by A55,YELLOW_1:3; w c= x by A54,YELLOW_1:3; then w c= x /\ y by A56,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A57: x = 2 & y = 3\1; 0 in Z by ENUMSET1:def 3; then reconsider z = 0 as Element of N by YELLOW_1:1; take z; A58: z c= y; z c= x; hence z <= x & z <= y by A58,YELLOW_1:3; let z9 be Element of N; assume that A59: z9 <= x and A60: z9 <= y; A61: z9 c= 3\1 by A57,A60,YELLOW_1:3; A62: now assume z9= 2; then 0 in z9 by CARD_1:50,TARSKI:def 2; hence contradiction by A61,Th3,TARSKI:def 2; end; A63: z9 c= 2 by A57,A59,YELLOW_1:3; A64: now assume z9= 3; then A65: 2 in z9 by CARD_1:51,ENUMSET1:def 1; not 2 in 2; hence contradiction by A63,A65; end; A66: now assume z9= 3\2; then A67: 2 in z9 by Th4,TARSKI:def 1; not 2 in 2; hence contradiction by A63,A67; end; A68: now assume z9= 3\1; then A69: 2 in z9 by Th3,TARSKI:def 2; not 2 in 2; hence contradiction by A63,A69; end; z9 is Element of Z by YELLOW_1:1; hence thesis by A68,A62,A66,A64,ENUMSET1:def 3; end; suppose x = 2 & y = 2; then reconsider z = x /\ y as Element of N; take z; A70: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A70,YELLOW_1:3; let w be Element of N; assume that A71: w <= x and A72: w <= y; A73: w c= y by A72,YELLOW_1:3; w c= x by A71,YELLOW_1:3; then w c= x /\ y by A73,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A74: x = 2 & y = 3\2; 2 misses (3\2) by XBOOLE_1:79; then 2 /\ (3\2) = 0; then x /\ y in Z by A74,ENUMSET1:def 3; then reconsider z = x /\ y as Element of N by YELLOW_1:1; take z; A75: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A75,YELLOW_1:3; let w be Element of N; assume that A76: w <= x and A77: w <= y; A78: w c= y by A77,YELLOW_1:3; w c= x by A76,YELLOW_1:3; then w c= x /\ y by A78,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A79: x = 2 & y = 3; Segm 2 c= Segm 3 by NAT_1:39; then reconsider z = x /\ y as Element of N by A79,XBOOLE_1:28; take z; A80: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A80,YELLOW_1:3; let w be Element of N; assume that A81: w <= x and A82: w <= y; A83: w c= y by A82,YELLOW_1:3; w c= x by A81,YELLOW_1:3; then w c= x /\ y by A83,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3\2 & y = 0; then reconsider z = x /\ y as Element of N; take z; A84: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A84,YELLOW_1:3; let w be Element of N; assume that A85: w <= x and A86: w <= y; A87: w c= y by A86,YELLOW_1:3; w c= x by A85,YELLOW_1:3; then w c= x /\ y by A87,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3\2 & y = 3\1; then reconsider z = x /\ y as Element of N by Th3,Th4,ZFMISC_1:13; take z; A88: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A88,YELLOW_1:3; let w be Element of N; assume that A89: w <= x and A90: w <= y; A91: w c= y by A90,YELLOW_1:3; w c= x by A89,YELLOW_1:3; then w c= x /\ y by A91,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A92: x = 3\2 & y = 2; 2 misses (3\2) by XBOOLE_1:79; then 2 /\ (3\2) = 0; then x /\ y in Z by A92,ENUMSET1:def 3; then reconsider z = x /\ y as Element of N by YELLOW_1:1; take z; A93: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A93,YELLOW_1:3; let w be Element of N; assume that A94: w <= x and A95: w <= y; A96: w c= y by A95,YELLOW_1:3; w c= x by A94,YELLOW_1:3; then w c= x /\ y by A96,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3\2 & y = 3\2; then reconsider z = x /\ y as Element of N; take z; A97: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A97,YELLOW_1:3; let w be Element of N; assume that A98: w <= x and A99: w <= y; A100: w c= y by A99,YELLOW_1:3; w c= x by A98,YELLOW_1:3; then w c= x /\ y by A100,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A101: x = 3\2 & y = 3; (3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49 .= 3\2; then reconsider z = x /\ y as Element of N by A101; take z; A102: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A102,YELLOW_1:3; let w be Element of N; assume that A103: w <= x and A104: w <= y; A105: w c= y by A104,YELLOW_1:3; w c= x by A103,YELLOW_1:3; then w c= x /\ y by A105,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3 & y = 0; then reconsider z = x /\ y as Element of N; take z; A106: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A106,YELLOW_1:3; let w be Element of N; assume that A107: w <= x and A108: w <= y; A109: w c= y by A108,YELLOW_1:3; w c= x by A107,YELLOW_1:3; then w c= x /\ y by A109,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A110: x = 3 & y = 3\1; (3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49 .= 3\1; then reconsider z = x /\ y as Element of N by A110; take z; A111: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A111,YELLOW_1:3; let w be Element of N; assume that A112: w <= x and A113: w <= y; A114: w c= y by A113,YELLOW_1:3; w c= x by A112,YELLOW_1:3; then w c= x /\ y by A114,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A115: x = 3 & y = 2; Segm 2 c= Segm 3 by NAT_1:39; then reconsider z = x /\ y as Element of N by A115,XBOOLE_1:28; take z; A116: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A116,YELLOW_1:3; let w be Element of N; assume that A117: w <= x and A118: w <= y; A119: w c= y by A118,YELLOW_1:3; w c= x by A117,YELLOW_1:3; then w c= x /\ y by A119,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose A120: x = 3 & y = 3\2; (3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49 .= 3\2; then reconsider z = x /\ y as Element of N by A120; take z; A121: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A121,YELLOW_1:3; let w be Element of N; assume that A122: w <= x and A123: w <= y; A124: w c= y by A123,YELLOW_1:3; w c= x by A122,YELLOW_1:3; then w c= x /\ y by A124,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; suppose x = 3 & y = 3; then reconsider z = x /\ y as Element of N; take z; A125: z c= y by XBOOLE_1:17; z c= x by XBOOLE_1:17; hence z <= x & z <= y by A125,YELLOW_1:3; let w be Element of N; assume that A126: w <= x and A127: w <= y; A128: w c= y by A127,YELLOW_1:3; w c= x by A126,YELLOW_1:3; then w c= x /\ y by A128,XBOOLE_1:19; hence thesis by YELLOW_1:3; end; end; end; now let x,y be set; assume that A129: x in Z and A130: y in Z; A131: x=0 or x=3\1 or x=2 or x=3\2 or x=3 by A129,ENUMSET1:def 3; Segm 2 c= Segm 3 by NAT_1:39; then A132: 2 \/ 3 = 3 by XBOOLE_1:12; A133: 2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39; A134: (3\1) \/ 2 = {0,1,1,2} by Th3,CARD_1:50,ENUMSET1:5 .= {1,1,0,2} by ENUMSET1:67 .= {1,0,2} by ENUMSET1:31 .= {0,1,2} by ENUMSET1:58; A135: (3\1) \/ 3 = 3 by XBOOLE_1:12; A136: y=0 or y=3\1 or y=2 or y=3\2 or y=3 by A130,ENUMSET1:def 3; A137: (3\2) \/ 3 = 3 by XBOOLE_1:12; (3\1) \/ (3\2) = {1,2} by Th3,Th4,ZFMISC_1:9; hence x \/ y in Z by A131,A136,A134,A135,A133,A132,A137,Th3,CARD_1:51 ,ENUMSET1:def 3; end; hence thesis by A1,YELLOW_1:11; end; end; definition func M_3 -> RelStr equals InclPoset{ 0, 1, 2 \ 1, 3 \ 2, 3 }; correctness; end; registration cluster M_3 -> strict reflexive transitive antisymmetric; correctness; cluster M_3 -> with_infima with_suprema; correctness proof set Z = { 0, 1, 2 \ 1, 3 \ 2, 3 }; set N = InclPoset Z; A1: N is with_suprema proof let x,y be Element of N; A2: Z = the carrier of N by YELLOW_1:1; thus ex z being Element of N st x <= z & y <= z & for z9 being Element of N st x <= z9 & y <= z9 holds z <= z9 proof per cases by A2,ENUMSET1:def 3; suppose x=0 & y=0; then reconsider z = x \/ y as Element of N; take z; A3: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A3,YELLOW_1:3; let w be Element of N; assume that A4: x <= w and A5: y <= w; A6: y c= w by A5,YELLOW_1:3; x c= w by A4,YELLOW_1:3; then x \/ y c= w by A6,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=0 & y=1; then reconsider z = x \/ y as Element of N; take z; A7: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A7,YELLOW_1:3; let w be Element of N; assume that A8: x <= w and A9: y <= w; A10: y c= w by A9,YELLOW_1:3; x c= w by A8,YELLOW_1:3; then x \/ y c= w by A10,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=0 & y=2\1; then reconsider z = x \/ y as Element of N; take z; A11: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A11,YELLOW_1:3; let w be Element of N; assume that A12: x <= w and A13: y <= w; A14: y c= w by A13,YELLOW_1:3; x c= w by A12,YELLOW_1:3; then x \/ y c= w by A14,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=0 & y=3\2; then reconsider z = x \/ y as Element of N; take z; A15: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A15,YELLOW_1:3; let w be Element of N; assume that A16: x <= w and A17: y <= w; A18: y c= w by A17,YELLOW_1:3; x c= w by A16,YELLOW_1:3; then x \/ y c= w by A18,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=0 & y=3; then reconsider z = x \/ y as Element of N; take z; A19: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A19,YELLOW_1:3; let w be Element of N; assume that A20: x <= w and A21: y <= w; A22: y c= w by A21,YELLOW_1:3; x c= w by A20,YELLOW_1:3; then x \/ y c= w by A22,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=1 & y=0; then reconsider z = x \/ y as Element of N; take z; A23: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A23,YELLOW_1:3; let w be Element of N; assume that A24: x <= w and A25: y <= w; A26: y c= w by A25,YELLOW_1:3; x c= w by A24,YELLOW_1:3; then x \/ y c= w by A26,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=1 & y=1; then reconsider z = x \/ y as Element of N; take z; A27: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A27,YELLOW_1:3; let w be Element of N; assume that A28: x <= w and A29: y <= w; A30: y c= w by A29,YELLOW_1:3; x c= w by A28,YELLOW_1:3; then x \/ y c= w by A30,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A31: x=1 & y=2\1; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; x c= z & y c= z proof thus x c= z proof let X be object; assume X in x; then X=0 by A31,CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; let X be object; assume X in y; then X=1 by A31,Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; hence x <= z & y <= z by YELLOW_1:3; let z9 be Element of N; assume that A32: x <= z9 and A33: y <= z9; A34: z9 is Element of Z by YELLOW_1:1; A35: 2\1 c= z9 by A31,A33,YELLOW_1:3; A36: now 1 in 2\1 by Th2,TARSKI:def 1; then A37: 1 in z9 by A35; assume z9= 1; hence contradiction by A37; end; A38: 1 c= z9 by A31,A32,YELLOW_1:3; A39: now A40: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 2\1; hence contradiction by A38,A40,Th2,TARSKI:def 1; end; A41: now A42: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 3\2; hence contradiction by A38,A42,Th4,TARSKI:def 1; end; z9 <> 0 by A38; hence thesis by A34,A36,A39,A41,ENUMSET1:def 3; end; suppose A43: x=1 & y=3\2; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; x c= z proof let X be object; assume X in x; then X=0 by A43,CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; hence x <= z & y <= z by A43,YELLOW_1:3; let z9 be Element of N; assume that A44: x <= z9 and A45: y <= z9; A46: z9 is Element of Z by YELLOW_1:1; A47: 3\2 c= z9 by A43,A45,YELLOW_1:3; A48: now assume A49: z9= 1; 2 in 3\2 by Th4,TARSKI:def 1; hence contradiction by A47,A49,CARD_1:49,TARSKI:def 1; end; A50: 1 c= z9 by A43,A44,YELLOW_1:3; A51: now A52: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 2\1; hence contradiction by A50,A52,Th2,TARSKI:def 1; end; A53: now A54: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 3\2; hence contradiction by A50,A54,Th4,TARSKI:def 1; end; z9 <> 0 by A50; hence thesis by A46,A48,A51,A53,ENUMSET1:def 3; end; suppose A55: x=1 & y=3; Segm 1 c= Segm 3 proof let X be object; assume X in Segm 1; then X=0 by CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then reconsider z = x \/ y as Element of N by A55,XBOOLE_1:12; take z; A56: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A56,YELLOW_1:3; let w be Element of N; assume that A57: x <= w and A58: y <= w; A59: y c= w by A58,YELLOW_1:3; x c= w by A57,YELLOW_1:3; then x \/ y c= w by A59,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=2\1 & y=0; then reconsider z = x \/ y as Element of N; take z; A60: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A60,YELLOW_1:3; let w be Element of N; assume that A61: x <= w and A62: y <= w; A63: y c= w by A62,YELLOW_1:3; x c= w by A61,YELLOW_1:3; then x \/ y c= w by A63,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A64: x=2\1 & y=1; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; x c= z & y c= z proof thus x c= z proof let X be object; assume X in x; then X=1 by A64,Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; let X be object; assume X in y; then X=0 by A64,CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; hence x <= z & y <= z by YELLOW_1:3; let z9 be Element of N; assume that A65: x <= z9 and A66: y <= z9; A67: z9 is Element of Z by YELLOW_1:1; A68: 2\1 c= z9 by A64,A65,YELLOW_1:3; A69: now 1 in 2\1 by Th2,TARSKI:def 1; then A70: 1 in z9 by A68; assume z9= 1; hence contradiction by A70; end; A71: 1 c= z9 by A64,A66,YELLOW_1:3; A72: now A73: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 2\1; hence contradiction by A71,A73,Th2,TARSKI:def 1; end; A74: now A75: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 3\2; hence contradiction by A71,A75,Th4,TARSKI:def 1; end; z9 <> 0 by A71; hence thesis by A67,A69,A72,A74,ENUMSET1:def 3; end; suppose x=2\1 & y=2\1; then reconsider z = x \/ y as Element of N; take z; A76: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A76,YELLOW_1:3; let w be Element of N; assume that A77: x <= w and A78: y <= w; A79: y c= w by A78,YELLOW_1:3; x c= w by A77,YELLOW_1:3; then x \/ y c= w by A79,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A80: x=2\1 & y=3\2; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; x c= z & y c= z proof thus x c= z proof let X be object; assume X in x; then X=1 by A80,Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; let X be object; assume X in y; hence thesis by A80; end; hence x <= z & y <= z by YELLOW_1:3; let z9 be Element of N; assume that A81: x <= z9 and A82: y <= z9; A83: z9 is Element of Z by YELLOW_1:1; A84: 3\2 c= z9 by A80,A82,YELLOW_1:3; A85: now assume A86: z9= 2\1; 2 in 3\2 by Th4,TARSKI:def 1; hence contradiction by A84,A86,Th2,TARSKI:def 1; end; A87: 2\1 c= z9 by A80,A81,YELLOW_1:3; A88: now assume A89: z9= 3\2; 1 in 2\1 by Th2,TARSKI:def 1; hence contradiction by A87,A89,Th4,TARSKI:def 1; end; A90: now 1 in 2\1 by Th2,TARSKI:def 1; then A91: 1 in z9 by A87; assume z9= 1; hence contradiction by A91; end; z9 <> 0 by A87,Th2; hence thesis by A83,A90,A85,A88,ENUMSET1:def 3; end; suppose A92: x=2\1 & y=3; 2\1 c= 3 proof let X be object; assume X in 2\1; then X=1 by Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then reconsider z = x \/ y as Element of N by A92,XBOOLE_1:12; take z; A93: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A93,YELLOW_1:3; let w be Element of N; assume that A94: x <= w and A95: y <= w; A96: y c= w by A95,YELLOW_1:3; x c= w by A94,YELLOW_1:3; then x \/ y c= w by A96,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=3\2 & y=0; then reconsider z = x \/ y as Element of N; take z; A97: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A97,YELLOW_1:3; let w be Element of N; assume that A98: x <= w and A99: y <= w; A100: y c= w by A99,YELLOW_1:3; x c= w by A98,YELLOW_1:3; then x \/ y c= w by A100,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A101: x=3\2 & y=1; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; y c= z proof let X be object; assume X in y; then X=0 by A101,CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; hence x <= z & y <= z by A101,YELLOW_1:3; let z9 be Element of N; assume that A102: x <= z9 and A103: y <= z9; A104: z9 is Element of Z by YELLOW_1:1; A105: 3\2 c= z9 by A101,A102,YELLOW_1:3; A106: now assume A107: z9= 1; 2 in 3\2 by Th4,TARSKI:def 1; hence contradiction by A105,A107,CARD_1:49,TARSKI:def 1; end; A108: 1 c= z9 by A101,A103,YELLOW_1:3; A109: now A110: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 2\1; hence contradiction by A108,A110,Th2,TARSKI:def 1; end; A111: now A112: 0 in 1 by CARD_1:49,TARSKI:def 1; assume z9= 3\2; hence contradiction by A108,A112,Th4,TARSKI:def 1; end; z9 <> 0 by A108; hence thesis by A104,A106,A109,A111,ENUMSET1:def 3; end; suppose A113: x=3\2 & y=2\1; 3 in Z by ENUMSET1:def 3; then reconsider z = 3 as Element of N by YELLOW_1:1; take z; x c= z & y c= z proof thus x c= z by A113; let X be object; assume X in y; then X=1 by A113,Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; hence x <= z & y <= z by YELLOW_1:3; let z9 be Element of N; assume that A114: x <= z9 and A115: y <= z9; A116: z9 is Element of Z by YELLOW_1:1; A117: 3\2 c= z9 by A113,A114,YELLOW_1:3; A118: now assume A119: z9= 2\1; 2 in 3\2 by Th4,TARSKI:def 1; hence contradiction by A117,A119,Th2,TARSKI:def 1; end; A120: 2\1 c= z9 by A113,A115,YELLOW_1:3; A121: now assume A122: z9= 3\2; 1 in 2\1 by Th2,TARSKI:def 1; hence contradiction by A120,A122,Th4,TARSKI:def 1; end; A123: now 1 in 2\1 by Th2,TARSKI:def 1; then A124: 1 in z9 by A120; assume z9= 1; hence contradiction by A124; end; z9 <> 0 by A120,Th2; hence thesis by A116,A123,A118,A121,ENUMSET1:def 3; end; suppose x=3\2 & y=3\2; then reconsider z = x \/ y as Element of N; take z; A125: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A125,YELLOW_1:3; let w be Element of N; assume that A126: x <= w and A127: y <= w; A128: y c= w by A127,YELLOW_1:3; x c= w by A126,YELLOW_1:3; then x \/ y c= w by A128,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=3\2 & y=3; then reconsider z = x \/ y as Element of N by XBOOLE_1:12; take z; A129: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A129,YELLOW_1:3; let w be Element of N; assume that A130: x <= w and A131: y <= w; A132: y c= w by A131,YELLOW_1:3; x c= w by A130,YELLOW_1:3; then x \/ y c= w by A132,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=3 & y=0; then reconsider z = x \/ y as Element of N; take z; A133: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A133,YELLOW_1:3; let w be Element of N; assume that A134: x <= w and A135: y <= w; A136: y c= w by A135,YELLOW_1:3; x c= w by A134,YELLOW_1:3; then x \/ y c= w by A136,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A137: x=3 & y=1; Segm 1 c= Segm 3 proof let X be object; assume X in Segm 1; then X=0 by CARD_1:49,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then reconsider z = x \/ y as Element of N by A137,XBOOLE_1:12; take z; A138: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A138,YELLOW_1:3; let w be Element of N; assume that A139: x <= w and A140: y <= w; A141: y c= w by A140,YELLOW_1:3; x c= w by A139,YELLOW_1:3; then x \/ y c= w by A141,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose A142: x=3 & y=2\1; 2\1 c= 3 proof let X be object; assume X in 2\1; then X=1 by Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then reconsider z = x \/ y as Element of N by A142,XBOOLE_1:12; take z; A143: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A143,YELLOW_1:3; let w be Element of N; assume that A144: x <= w and A145: y <= w; A146: y c= w by A145,YELLOW_1:3; x c= w by A144,YELLOW_1:3; then x \/ y c= w by A146,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=3 & y=3\2; then reconsider z = x \/ y as Element of N by XBOOLE_1:12; take z; A147: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A147,YELLOW_1:3; let w be Element of N; assume that A148: x <= w and A149: y <= w; A150: y c= w by A149,YELLOW_1:3; x c= w by A148,YELLOW_1:3; then x \/ y c= w by A150,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; suppose x=3 & y=3; then reconsider z = x \/ y as Element of N; take z; A151: y c= z by XBOOLE_1:7; x c= z by XBOOLE_1:7; hence x <= z & y <= z by A151,YELLOW_1:3; let w be Element of N; assume that A152: x <= w and A153: y <= w; A154: y c= w by A153,YELLOW_1:3; x c= w by A152,YELLOW_1:3; then x \/ y c= w by A154,XBOOLE_1:8; hence thesis by YELLOW_1:3; end; end; end; now now let x be object; assume A155: x in (2\1) /\ (3\2); then x in (2\1) by XBOOLE_0:def 4; then A156: x=1 by Th2,TARSKI:def 1; x in (3\2) by A155,XBOOLE_0:def 4; hence contradiction by A156,Th4,TARSKI:def 1; end; then A157: (2\1) /\ (3\2) = 0 by XBOOLE_0:def 1; A158: (3\2) /\ 3 = 3\2 by XBOOLE_1:28; (2\1) c= 3 proof let x be object; assume x in 2\1; then x = 1 by Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then A159: (2\1) /\ 3 = 2\1 by XBOOLE_1:28; Segm 1 c= Segm 3 by NAT_1:39; then A160: 1 /\ 3 = 1 by XBOOLE_1:28; now let x be object; assume A161: x in 1 /\ (3\2); then x in 1 by XBOOLE_0:def 4; then A162: x=0 by CARD_1:49,TARSKI:def 1; x in (3\2) by A161,XBOOLE_0:def 4; hence contradiction by A162,Th4,TARSKI:def 1; end; then A163: 1 /\ (3\2) = 0 by XBOOLE_0:def 1; 1 misses (2\1) by XBOOLE_1:79; then A164: 1 /\ (2\1) = 0; let x,y be set; assume that A165: x in Z and A166: y in Z; A167: y=0 or y=1 or y=2\1 or y=3\2 or y=3 by A166,ENUMSET1:def 3; x=0 or x=1 or x=2\1 or x=3\2 or x=3 by A165,ENUMSET1:def 3; hence x /\ y in Z by A167,A164,A163,A160,A157,A159,A158,ENUMSET1:def 3; end; hence thesis by A1,YELLOW_1:12; end; end; theorem Th9: for L being LATTICE holds (ex K being full Sublattice of L st N_5,K are_isomorphic) iff ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e proof set cn = the carrier of N_5; let L be LATTICE; A1: cn = {0, 3 \ 1, 2, 3 \ 2, 3} by YELLOW_1:1; thus (ex K being full Sublattice of L st N_5,K are_isomorphic) implies ex a, b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b "/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e proof reconsider td = 3\2 as Element of N_5 by A1,ENUMSET1:def 3; reconsider dw = 2 as Element of N_5 by A1,ENUMSET1:def 3; reconsider t = 3 as Element of N_5 by A1,ENUMSET1:def 3; reconsider tj = 3\1 as Element of N_5 by A1,ENUMSET1:def 3; reconsider cl = the carrier of L as non empty set; reconsider z = 0 as Element of N_5 by A1,ENUMSET1:def 3; given K being full Sublattice of L such that A2: N_5,K are_isomorphic; consider f being Function of N_5,K such that A3: f is isomorphic by A2; A4: K is non empty by A3,WAYBEL_0:def 38; then A5: f is one-to-one monotone by A3,WAYBEL_0:def 38; reconsider K as non empty SubRelStr of L by A3,WAYBEL_0:def 38; reconsider ck = the carrier of K as non empty set; A6: ck = rng f by A3,WAYBEL_0:66; reconsider g=f as Function of cn,ck; reconsider a=g.z,b=g.td,c =g.dw,d=g.tj,e=g.t as Element of K; reconsider ck as non empty Subset of cl by YELLOW_0:def 13; A7: b in ck; A8: c in ck; A9: e in ck; A10: d in ck; a in ck; then reconsider A=a,B=b,C=c,D=d,E=e as Element of L by A7,A8,A10,A9; take A,B,C,D,E; thus A<>B by A5,Th4,WAYBEL_1:def 1; thus A<>C by A5,WAYBEL_1:def 1; thus A<>D by A5,Th3,WAYBEL_1:def 1; thus A<>E by A5,WAYBEL_1:def 1; now assume f.td = f.dw; then A11: td = dw by A4,A5,WAYBEL_1:def 1; 2 in td by Th4,TARSKI:def 1; hence contradiction by A11; end; hence B<>C; now A12: 1 in tj by Th3,TARSKI:def 2; assume A13: f.td = f.tj; not 1 in td by Th4,TARSKI:def 1; hence contradiction by A4,A5,A13,A12,WAYBEL_1:def 1; end; hence B<>D; now A14: 1 in t by CARD_1:51,ENUMSET1:def 1; assume A15: f.td = f.t; not 1 in td by Th4,TARSKI:def 1; hence contradiction by A4,A5,A15,A14,WAYBEL_1:def 1; end; hence B<>E; now assume f.dw = f.tj; then A16: dw = tj by A4,A5,WAYBEL_1:def 1; 2 in tj by Th3,TARSKI:def 2; hence contradiction by A16; end; hence C<>D; thus C<>E by A5,WAYBEL_1:def 1; now A17: 0 in t by CARD_1:51,ENUMSET1:def 1; assume A18: f.tj = f.t; not 0 in tj by Th3,TARSKI:def 2; hence contradiction by A4,A5,A18,A17,WAYBEL_1:def 1; end; hence D<>E; z c= td; then z <= td by YELLOW_1:3; then a <= b by A3,WAYBEL_0:66; then A <= B by YELLOW_0:59; hence A "/\" B = A by YELLOW_0:25; z c= dw; then z <= dw by YELLOW_1:3; then a <= c by A3,WAYBEL_0:66; then A <= C by YELLOW_0:59; hence A "/\" C = A by YELLOW_0:25; Segm 2 c= Segm 3 by NAT_1:39; then dw <= t by YELLOW_1:3; then c <= e by A3,WAYBEL_0:66; then C <= E by YELLOW_0:59; hence C"/\"E = C by YELLOW_0:25; tj <= t by YELLOW_1:3; then d <= e by A3,WAYBEL_0:66; then D <= E by YELLOW_0:59; hence D"/\"E = D by YELLOW_0:25; thus B"/\"C = A proof A19: now assume B"/\"C = D; then D <= C by YELLOW_0:23; then d <= c by YELLOW_0:60; then tj <= dw by A3,WAYBEL_0:66; then A20: tj c= dw by YELLOW_1:3; 2 in tj by Th3,TARSKI:def 2; then 2 in 2 by A20; hence contradiction; end; A21: now assume B"/\"C = E; then E <= C by YELLOW_0:23; then e <= c by YELLOW_0:60; then t <= dw by A3,WAYBEL_0:66; then A22: t c= dw by YELLOW_1:3; 2 in t by CARD_1:51,ENUMSET1:def 1; then 2 in 2 by A22; hence contradiction; end; A23: now assume B"/\"C = B; then B <= C by YELLOW_0:25; then b <= c by YELLOW_0:60; then td <= dw by A3,WAYBEL_0:66; then A24: td c= dw by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; then 2 in 2 by A24; hence contradiction; end; A25: now assume B"/\"C = C; then C <= B by YELLOW_0:25; then c <= b by YELLOW_0:60; then dw <= td by A3,WAYBEL_0:66; then A26: dw c= td by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A26,Th4,TARSKI:def 1; end; ex_inf_of {B,C},L by YELLOW_0:21; then inf{B,C} in the carrier of K by YELLOW_0:def 16; then B"/\"C in rng f by A6,YELLOW_0:40; then ex x being object st x in dom f & B"/\"C = f.x by FUNCT_1:def 3; hence thesis by A1,A23,A25,A19,A21,ENUMSET1:def 3; end; td <= tj by Lm1,YELLOW_1:3; then b <= d by A3,WAYBEL_0:66; then B <= D by YELLOW_0:59; hence B"/\"D = B by YELLOW_0:25; thus C"/\"D = A proof A27: now assume C"/\"D = D; then D <= C by YELLOW_0:23; then d <= c by YELLOW_0:60; then tj <= dw by A3,WAYBEL_0:66; then A28: tj c= dw by YELLOW_1:3; 2 in tj by Th3,TARSKI:def 2; then 2 in 2 by A28; hence contradiction; end; A29: now assume C"/\"D = E; then E <= C by YELLOW_0:23; then e <= c by YELLOW_0:60; then t <= dw by A3,WAYBEL_0:66; then A30: t c= dw by YELLOW_1:3; 2 in t by CARD_1:51,ENUMSET1:def 1; then 2 in 2 by A30; hence contradiction; end; A31: now assume C"/\"D = B; then B <= C by YELLOW_0:23; then b <= c by YELLOW_0:60; then td <= dw by A3,WAYBEL_0:66; then A32: td c= dw by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; then 2 in 2 by A32; hence contradiction; end; A33: now assume C"/\"D = C; then C <= D by YELLOW_0:25; then c <= d by YELLOW_0:60; then dw <= tj by A3,WAYBEL_0:66; then A34: dw c= tj by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A34,Th3,TARSKI:def 2; end; ex_inf_of {C,D},L by YELLOW_0:21; then inf{C,D} in the carrier of K by YELLOW_0:def 16; then C"/\"D in rng f by A6,YELLOW_0:40; then ex x being object st x in dom f & C"/\"D = f.x by FUNCT_1:def 3; hence thesis by A1,A31,A33,A27,A29,ENUMSET1:def 3; end; thus B"\/"C = E proof A35: now assume B"\/"C = C; then C >= B by YELLOW_0:24; then c >= b by YELLOW_0:60; then dw >= td by A3,WAYBEL_0:66; then A36: td c= dw by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; then 2 in 2 by A36; hence contradiction; end; A37: now assume B"\/"C = D; then D >= C by YELLOW_0:22; then d >= c by YELLOW_0:60; then tj >= dw by A3,WAYBEL_0:66; then A38: dw c= tj by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A38,Th3,TARSKI:def 2; end; A39: now assume B"\/"C = B; then B >= C by YELLOW_0:24; then b >= c by YELLOW_0:60; then td >= dw by A3,WAYBEL_0:66; then A40: dw c= td by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A40,Th4,TARSKI:def 1; end; A41: now assume B"\/"C = A; then A >= C by YELLOW_0:22; then a >= c by YELLOW_0:60; then z >= dw by A3,WAYBEL_0:66; then dw c= z by YELLOW_1:3; hence contradiction; end; ex_sup_of {B,C},L by YELLOW_0:20; then sup{B,C} in the carrier of K by YELLOW_0:def 17; then B"\/"C in rng f by A6,YELLOW_0:41; then ex x being object st x in dom f & B"\/"C = f.x by FUNCT_1:def 3; hence thesis by A1,A39,A35,A37,A41,ENUMSET1:def 3; end; thus C"\/"D = E proof A42: now assume C"\/"D = D; then D >= C by YELLOW_0:22; then d >= c by YELLOW_0:60; then tj >= dw by A3,WAYBEL_0:66; then A43: dw c= tj by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A43,Th3,TARSKI:def 2; end; A44: now assume C"\/"D = C; then C >= D by YELLOW_0:24; then c >= d by YELLOW_0:60; then dw >= tj by A3,WAYBEL_0:66; then A45: tj c= dw by YELLOW_1:3; 2 in tj by Th3,TARSKI:def 2; hence contradiction by A45,CARD_1:50,TARSKI:def 2; end; A46: now assume C"\/"D = B; then B >= C by YELLOW_0:22; then b >= c by YELLOW_0:60; then td >= dw by A3,WAYBEL_0:66; then A47: dw c= td by YELLOW_1:3; 0 in dw by CARD_1:50,TARSKI:def 2; hence contradiction by A47,Th4,TARSKI:def 1; end; A48: now assume C"\/"D = A; then A >= C by YELLOW_0:22; then a >= c by YELLOW_0:60; then z >= dw by A3,WAYBEL_0:66; then dw c= z by YELLOW_1:3; hence contradiction; end; ex_sup_of {C,D},L by YELLOW_0:20; then sup{C,D} in the carrier of K by YELLOW_0:def 17; then C"\/"D in rng f by A6,YELLOW_0:41; then ex x being object st x in dom f & C"\/"D = f.x by FUNCT_1:def 3; hence thesis by A1,A46,A44,A42,A48,ENUMSET1:def 3; end; end; thus (ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d "/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e)) implies ex K being full Sublattice of L st N_5,K are_isomorphic proof given a,b,c,d,e being Element of L such that AAA: a,b,c,d,e are_mutually_distinct and A59: a"/\"b = a and A60: a"/\"c = a and A61: c"/\"e = c and A62: d"/\"e = d and A63: b"/\"c = a and A64: b"/\"d = b and A65: c"/\"d = a and A66: b"\/"c = e and A67: c"\/"d = e; set ck = {a,b,c,d,e}; reconsider ck as Subset of L; set K = subrelstr ck; A68: the carrier of K = ck by YELLOW_0:def 15; A69: K is meet-inheriting proof let x,y be Element of L; assume that A70: x in the carrier of K and A71: y in the carrier of K and ex_inf_of {x,y},L; per cases by A68,A70,A71,ENUMSET1:def 3; suppose x=a & y=a; then inf{x,y} = a"/\"a by YELLOW_0:40; then inf{x,y} = a by YELLOW_5:2; hence thesis by A68,ENUMSET1:def 3; end; suppose x=a & y=b; then inf{x,y} = a"/\"b by YELLOW_0:40; hence thesis by A59,A68,ENUMSET1:def 3; end; suppose x=a & y=c; then inf{x,y} = a"/\"c by YELLOW_0:40; hence thesis by A60,A68,ENUMSET1:def 3; end; suppose A72: x=a & y=d; A73: b <= d by A64,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then a <= d by A73,ORDERS_2:3; then a"/\"d = a by YELLOW_0:25; then inf {x,y} = a by A72,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose A74: x=a & y=e; A75: c <= e by A61,YELLOW_0:25; a <= c by A60,YELLOW_0:25; then a <= e by A75,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then inf {x,y} = a by A74,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose x=b & y=a; then inf{x,y} = a"/\"b by YELLOW_0:40; hence thesis by A59,A68,ENUMSET1:def 3; end; suppose x=b & y=b; then inf{x,y} = b"/\"b by YELLOW_0:40; then inf{x,y} = b by YELLOW_5:2; hence thesis by A68,ENUMSET1:def 3; end; suppose x=b & y=c; then inf{x,y} = b"/\"c by YELLOW_0:40; hence thesis by A63,A68,ENUMSET1:def 3; end; suppose x=b & y=d; then inf{x,y} = b"/\"d by YELLOW_0:40; hence thesis by A64,A68,ENUMSET1:def 3; end; suppose A76: x=b & y=e; A77: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then b <= e by A77,ORDERS_2:3; then b"/\"e = b by YELLOW_0:25; then inf {x,y} = b by A76,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose x=c & y=a; then inf{x,y} = a"/\"c by YELLOW_0:40; hence thesis by A60,A68,ENUMSET1:def 3; end; suppose x=c & y=b; then inf{x,y} = b"/\"c by YELLOW_0:40; hence thesis by A63,A68,ENUMSET1:def 3; end; suppose x=c & y=c; then inf{x,y} = c"/\"c by YELLOW_0:40; then inf{x,y} = c by YELLOW_5:2; hence thesis by A68,ENUMSET1:def 3; end; suppose x=c & y=d; then inf{x,y} = c"/\"d by YELLOW_0:40; hence thesis by A65,A68,ENUMSET1:def 3; end; suppose x=c & y=e; then inf{x,y} = c"/\"e by YELLOW_0:40; hence thesis by A61,A68,ENUMSET1:def 3; end; suppose A78: x=d & y=a; A79: b <= d by A64,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then a <= d by A79,ORDERS_2:3; then a"/\"d = a by YELLOW_0:25; then inf {x,y} = a by A78,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose x=d & y=b; then inf{x,y} = b"/\"d by YELLOW_0:40; hence thesis by A64,A68,ENUMSET1:def 3; end; suppose x=d & y=c; then inf{x,y} = c"/\"d by YELLOW_0:40; hence thesis by A65,A68,ENUMSET1:def 3; end; suppose x=d & y=d; then inf{x,y} = d"/\"d by YELLOW_0:40; then inf{x,y} = d by YELLOW_5:2; hence thesis by A68,ENUMSET1:def 3; end; suppose x=d & y=e; then inf{x,y} = d"/\"e by YELLOW_0:40; hence thesis by A62,A68,ENUMSET1:def 3; end; suppose A80: x=e & y=a; A81: c <= e by A61,YELLOW_0:25; a <= c by A60,YELLOW_0:25; then a <= e by A81,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then inf {x,y} = a by A80,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose A82: x=e & y=b; A83: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then b <= e by A83,ORDERS_2:3; then b"/\"e = b by YELLOW_0:25; then inf {x,y} = b by A82,YELLOW_0:40; hence thesis by A68,ENUMSET1:def 3; end; suppose x=e & y=c; then inf{x,y} = c"/\"e by YELLOW_0:40; hence thesis by A61,A68,ENUMSET1:def 3; end; suppose x=e & y=d; then inf{x,y} = d"/\"e by YELLOW_0:40; hence thesis by A62,A68,ENUMSET1:def 3; end; suppose x=e & y=e; then inf{x,y} = e"/\"e by YELLOW_0:40; then inf{x,y} = e by YELLOW_5:2; hence thesis by A68,ENUMSET1:def 3; end; end; K is join-inheriting proof let x,y be Element of L; assume that A84: x in the carrier of K and A85: y in the carrier of K and ex_sup_of {x,y},L; per cases by A68,A84,A85,ENUMSET1:def 3; suppose x=a & y=a; then sup{x,y} = a"\/"a by YELLOW_0:41; then sup{x,y} = a by YELLOW_5:1; hence thesis by A68,ENUMSET1:def 3; end; suppose x=a & y=b; then x"\/"y = b by A59,Th5; then sup{x,y} = b by YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose x=a & y=c; then x"\/"y = c by A60,Th5; then sup{x,y} = c by YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A86: x=a & y=d; A87: b <= d by A64,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then a <= d by A87,ORDERS_2:3; then a"/\"d = a by YELLOW_0:25; then a"\/"d = d by Th5; then sup {x,y} = d by A86,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A88: x=a & y=e; A89: c <= e by A61,YELLOW_0:25; a <= c by A60,YELLOW_0:25; then a <= e by A89,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then a"\/"e = e by Th5; then sup {x,y} = e by A88,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A90: x=b & y=a; a"\/"b = b by A59,Th5; then sup{x,y} = b by A90,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose x=b & y=b; then sup{x,y} = b"\/"b by YELLOW_0:41; then sup{x,y} = b by YELLOW_5:1; hence thesis by A68,ENUMSET1:def 3; end; suppose x=b & y=c; then sup{x,y} = b"\/"c by YELLOW_0:41; hence thesis by A66,A68,ENUMSET1:def 3; end; suppose A91: x=b & y=d; b"\/"d = d by A64,Th5; then sup{x,y} = d by A91,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A92: x=b & y=e; A93: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then b <= e by A93,ORDERS_2:3; then b"/\"e = b by YELLOW_0:25; then b"\/"e = e by Th5; then sup {x,y} = e by A92,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A94: x=c & y=a; c"\/"a = c by A60,Th5; then sup{x,y} = c by A94,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose x=c & y=b; then sup{x,y} = b"\/"c by YELLOW_0:41; hence thesis by A66,A68,ENUMSET1:def 3; end; suppose x=c & y=c; then sup{x,y} = c"\/"c by YELLOW_0:41; then sup{x,y} = c by YELLOW_5:1; hence thesis by A68,ENUMSET1:def 3; end; suppose x=c & y=d; then sup{x,y} = c"\/"d by YELLOW_0:41; hence thesis by A67,A68,ENUMSET1:def 3; end; suppose A95: x=c & y=e; c"\/"e = e by A61,Th5; then sup{x,y} = e by A95,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A96: x=d & y=a; A97: b <= d by A64,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then a <= d by A97,ORDERS_2:3; then a"/\"d = a by YELLOW_0:25; then a"\/"d = d by Th5; then sup {x,y} = d by A96,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A98: x=d & y=b; b"\/"d = d by A64,Th5; then sup{x,y} = d by A98,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose x=d & y=c; then sup{x,y} = c"\/"d by YELLOW_0:41; hence thesis by A67,A68,ENUMSET1:def 3; end; suppose x=d & y=d; then sup{x,y} = d"\/"d by YELLOW_0:41; then sup{x,y} = d by YELLOW_5:1; hence thesis by A68,ENUMSET1:def 3; end; suppose A99: x=d & y=e; d"\/"e = e by A62,Th5; then sup{x,y} = e by A99,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A100: x=e & y=a; A101: c <= e by A61,YELLOW_0:25; a <= c by A60,YELLOW_0:25; then a <= e by A101,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then a"\/"e = e by Th5; then sup {x,y} = e by A100,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A102: x=e & y=b; A103: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then b <= e by A103,ORDERS_2:3; then b"/\"e = b by YELLOW_0:25; then b"\/"e = e by Th5; then sup {x,y} = e by A102,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A104: x=e & y=c; c"\/"e = e by A61,Th5; then sup{x,y} = e by A104,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose A105: x=e & y=d; d"\/"e = e by A62,Th5; then sup{x,y} = e by A105,YELLOW_0:41; hence thesis by A68,ENUMSET1:def 3; end; suppose x=e & y=e; then sup{x,y} = e"\/"e by YELLOW_0:41; then sup{x,y} = e by YELLOW_5:1; hence thesis by A68,ENUMSET1:def 3; end; end; then reconsider K as non empty full Sublattice of L by A69,YELLOW_0:def 15; take K; thus N_5,K are_isomorphic proof reconsider t = 3 as Element of N_5 by A1,ENUMSET1:def 3; reconsider td = 3\2 as Element of N_5 by A1,ENUMSET1:def 3; reconsider dw = 2 as Element of N_5 by A1,ENUMSET1:def 3; A106: now assume A107: dw=td; 2 in td by Th4,TARSKI:def 1; hence contradiction by A107; end; A108: now assume A109: td=t; not 1 in td by Th4,TARSKI:def 1; hence contradiction by A109,CARD_1:51,ENUMSET1:def 1; end; reconsider tj = 3\1 as Element of N_5 by A1,ENUMSET1:def 3; reconsider z = 0 as Element of N_5 by A1,ENUMSET1:def 3; defpred P[object,object] means for X being Element of N_5 st X=$1 holds ((X = z implies $2 = a) & (X = td implies $2 = b) & (X = dw implies $2 = c) & (X = tj implies $2 = d) & (X = t implies $2 = e)); A110: now assume A111: tj=dw; 2 in tj by Th3,TARSKI:def 2; hence contradiction by A111; end; A112: now assume A113: tj=t; not 0 in tj by Th3,TARSKI:def 2; hence contradiction by A113,CARD_1:51,ENUMSET1:def 1; end; A114: now assume A115: tj=td; not 1 in td by Th4,TARSKI:def 1; hence contradiction by A115,Th3,TARSKI:def 2; end; A116: for x being object st x in cn ex y being object st y in ck & P[x,y] proof let x be object; assume A117: x in cn; per cases by A1,A117,ENUMSET1:def 3; suppose A118: x = 0; take y=a; thus y in ck by ENUMSET1:def 3; let X be Element of N_5; thus thesis by A118,Th3,Th4; end; suppose A119: x=3\1; take y=d; thus y in ck by ENUMSET1:def 3; let X be Element of N_5; thus thesis by A110,A114,A112,A119,Th3; end; suppose A120: x = 2; take y=c; thus y in ck by ENUMSET1:def 3; let X be Element of N_5; thus thesis by A110,A106,A120; end; suppose A121: x = 3 \ 2; take y=b; thus y in ck by ENUMSET1:def 3; let X be Element of N_5; thus thesis by A114,A106,A108,A121,Th4; end; suppose A122: x = 3; take y=e; thus y in ck by ENUMSET1:def 3; let X be Element of N_5; thus thesis by A112,A108,A122; end; end; consider f being Function of cn,ck such that A123: for x being object st x in cn holds P[x,f.x] from FUNCT_2:sch 1( A116); reconsider f as Function of N_5,K by A68; A124: now let x,y be Element of N_5; assume A125: f.x = f.y; thus x=y proof per cases by A1,ENUMSET1:def 3; suppose x = z & y = z; hence thesis; end; suppose x = tj & y = tj; hence thesis; end; suppose x = td & y = td; hence thesis; end; suppose x = dw & y = dw; hence thesis; end; suppose x = t & y = t; hence thesis; end; suppose A126: x = z & y = tj; then f.x=a by A123; hence thesis by AAA,A123,A125,A126; end; suppose A127: x = z & y = dw; then f.x=a by A123; hence thesis by AAA,A123,A125,A127; end; suppose A128: x = z & y = td; then f.x=a by A123; hence thesis by AAA,A123,A125,A128; end; suppose A129: x = z & y = t; then f.x=a by A123; hence thesis by AAA,A123,A125,A129; end; suppose A130: x = tj & y = z; then f.x=d by A123; hence thesis by AAA,A123,A125,A130; end; suppose A131: x = tj & y = dw; then f.x=d by A123; hence thesis by AAA,A123,A125,A131; end; suppose A132: x = tj & y = td; then f.x=d by A123; hence thesis by AAA,A123,A125,A132; end; suppose A133: x = tj & y = t; then f.x=d by A123; hence thesis by AAA,A123,A125,A133; end; suppose A134: x = dw & y = z; then f.x=c by A123; hence thesis by AAA,A123,A125,A134; end; suppose A135: x = dw & y = tj; then f.x=c by A123; hence thesis by AAA,A123,A125,A135; end; suppose A136: x = dw & y = td; then f.x=c by A123; hence thesis by AAA,A123,A125,A136; end; suppose A137: x = dw & y = t; then f.x=c by A123; hence thesis by AAA,A123,A125,A137; end; suppose A138: x = td & y = z; then f.x=b by A123; hence thesis by AAA,A123,A125,A138; end; suppose A139: x = td & y = tj; then f.x=b by A123; hence thesis by AAA,A123,A125,A139; end; suppose A140: x = td & y = dw; then f.x=b by A123; hence thesis by AAA,A123,A125,A140; end; suppose A141: x = td & y = t; then f.x=b by A123; hence thesis by AAA,A123,A125,A141; end; suppose A142: x = t & y = z; then f.x=e by A123; hence thesis by AAA,A123,A125,A142; end; suppose A143: x = t & y = tj; then f.x=e by A123; hence thesis by AAA,A123,A125,A143; end; suppose A144: x = t & y = dw; then f.x=e by A123; hence thesis by AAA,A123,A125,A144; end; suppose A145: x = t & y = td; then f.x=e by A123; hence thesis by AAA,A123,A125,A145; end; end; end; A146: rng f c= ck proof let y be object; assume y in rng f; then consider x being object such that A147: x in dom f and A148: y=f.x by FUNCT_1:def 3; reconsider x as Element of N_5 by A147; x = z or x = tj or x = dw or x = td or x = t by A1,ENUMSET1:def 3; then y=a or y=d or y=c or y=b or y=e by A123,A148; hence thesis by ENUMSET1:def 3; end; A149: dom f = the carrier of N_5 by FUNCT_2:def 1; ck c= rng f proof let y be object; assume A150: y in ck; per cases by A150,ENUMSET1:def 3; suppose A151: y=a; a = f.z by A123; hence thesis by A149,A151,FUNCT_1:def 3; end; suppose A152: y=b; b=f.td by A123; hence thesis by A149,A152,FUNCT_1:def 3; end; suppose A153: y=c; c = f.dw by A123; hence thesis by A149,A153,FUNCT_1:def 3; end; suppose A154: y=d; d=f.tj by A123; hence thesis by A149,A154,FUNCT_1:def 3; end; suppose A155: y=e; e=f.t by A123; hence thesis by A149,A155,FUNCT_1:def 3; end; end; then A156: rng f = ck by A146; A157: for x,y being Element of N_5 holds x <= y iff f.x <= f.y proof let x,y be Element of N_5; thus x <= y implies f.x <= f.y proof assume A158: x <= y; per cases by A1,ENUMSET1:def 3; suppose x=z & y=z; hence thesis; end; suppose A159: x=z & y=td; then A160: f.y = b by A123; A161: a <= b by A59,YELLOW_0:25; f.x = a by A123,A159; hence thesis by A160,A161,YELLOW_0:60; end; suppose A162: x=z & y=dw; then A163: f.y = c by A123; A164: a <= c by A60,YELLOW_0:25; f.x = a by A123,A162; hence thesis by A163,A164,YELLOW_0:60; end; suppose A165: x=z & y=tj; A166: b <= d by A64,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then A167: a <= d by A166,ORDERS_2:3; A168: f.y = d by A123,A165; f.x = a by A123,A165; hence thesis by A168,A167,YELLOW_0:60; end; suppose A169: x=z & y=t; A170: c <= e by A61,YELLOW_0:25; a <= c by A60,YELLOW_0:25; then A171: a <= e by A170,ORDERS_2:3; A172: f.y = e by A123,A169; f.x = a by A123,A169; hence thesis by A172,A171,YELLOW_0:60; end; suppose x=td & y=z; then td c= z by A158,YELLOW_1:3; hence thesis by Th4; end; suppose x=td & y=td; hence thesis; end; suppose A173: x=td & y=dw; A174: not 2 in dw; 2 in td by Th4,TARSKI:def 1; then not td c= dw by A174; hence thesis by A158,A173,YELLOW_1:3; end; suppose x=td & y=z; then td c= z by A158,YELLOW_1:3; hence thesis by Th4; end; suppose A175: x=td & y=tj; then A176: f.y = d by A123; A177: b <= d by A64,YELLOW_0:25; f.x = b by A123,A175; hence thesis by A176,A177,YELLOW_0:60; end; suppose A178: x=td & y=t; A179: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then A180: b <= e by A179,ORDERS_2:3; A181: f.y = e by A123,A178; f.x = b by A123,A178; hence thesis by A181,A180,YELLOW_0:60; end; suppose x=dw & y=z; then dw c= z by A158,YELLOW_1:3; hence thesis; end; suppose A182: x=dw & y=td; 0 in dw by CARD_1:50,TARSKI:def 2; then not dw c= td by Th4,TARSKI:def 1; hence thesis by A158,A182,YELLOW_1:3; end; suppose x=dw & y=dw; hence thesis; end; suppose A183: x=dw & y=tj; 0 in dw by CARD_1:50,TARSKI:def 2; then not dw c= tj by Th3,TARSKI:def 2; hence thesis by A158,A183,YELLOW_1:3; end; suppose A184: x=dw & y=t; then A185: f.y = e by A123; A186: c <= e by A61,YELLOW_0:25; f.x = c by A123,A184; hence thesis by A185,A186,YELLOW_0:60; end; suppose x=tj & y=z; then tj c= z by A158,YELLOW_1:3; hence thesis by Th3; end; suppose A187: x=tj & y=td; 1 in tj by Th3,TARSKI:def 2; then not tj c= td by Th4,TARSKI:def 1; hence thesis by A158,A187,YELLOW_1:3; end; suppose A188: x=tj & y=dw; A189: not 2 in dw; 2 in tj by Th3,TARSKI:def 2; then not tj c= dw by A189; hence thesis by A158,A188,YELLOW_1:3; end; suppose x=tj & y=tj; hence thesis; end; suppose A190: x=tj & y=t; then A191: f.y = e by A123; A192: d <= e by A62,YELLOW_0:25; f.x = d by A123,A190; hence thesis by A191,A192,YELLOW_0:60; end; suppose x=t & y=z; then t c= z by A158,YELLOW_1:3; hence thesis; end; suppose A193: x=t & y=td; 0 in t by CARD_1:51,ENUMSET1:def 1; then not t c= td by Th4,TARSKI:def 1; hence thesis by A158,A193,YELLOW_1:3; end; suppose A194: x=t & y=dw; A195: not 2 in dw; 2 in t by CARD_1:51,ENUMSET1:def 1; then not t c= dw by A195; hence thesis by A158,A194,YELLOW_1:3; end; suppose A196: x=t & y=tj; 0 in t by CARD_1:51,ENUMSET1:def 1; then not t c= tj by Th3,TARSKI:def 2; hence thesis by A158,A196,YELLOW_1:3; end; suppose x=t & y=t; hence thesis; end; end; thus f.x <= f.y implies x <= y proof A197: f.y in ck by A149,A156,FUNCT_1:def 3; A198: f.x in ck by A149,A156,FUNCT_1:def 3; assume A199: f.x <= f.y; per cases by A198,A197,ENUMSET1:def 3; suppose f.x = a & f.y = a; hence thesis by A124; end; suppose A200: f.x = a & f.y = b; f.z = a by A123; then z=x by A124,A200; then x c= y; hence thesis by YELLOW_1:3; end; suppose A201: f.x = a & f.y = c; f.z = a by A123; then z=x by A124,A201; then x c= y; hence thesis by YELLOW_1:3; end; suppose A202: f.x = a & f.y = d; f.z = a by A123; then z=x by A124,A202; then x c= y; hence thesis by YELLOW_1:3; end; suppose A203: f.x = a & f.y = e; f.z = a by A123; then z=x by A124,A203; then x c= y; hence thesis by YELLOW_1:3; end; suppose f.x = b & f.y = a; then b <= a by A199,YELLOW_0:59; hence thesis by AAA,A59,YELLOW_0:25; end; suppose f.x = b & f.y = b; hence thesis by A124; end; suppose f.x = b & f.y = c; then b <= c by A199,YELLOW_0:59; hence thesis by AAA,A63,YELLOW_0:25; end; suppose A204: f.x = b & f.y = d; f.tj = d by A123; then A205: y=tj by A124,A204; f.td = b by A123; then A206: x=td by A124,A204; Segm 1 c= Segm 2 by NAT_1:39; then x c= y by A206,A205,XBOOLE_1:34; hence thesis by YELLOW_1:3; end; suppose A207: f.x = b & f.y = e; f.t = e by A123; then A208: t = y by A124,A207; f.td = b by A123; then td=x by A124,A207; hence thesis by A208,YELLOW_1:3; end; suppose f.x = c & f.y = a; then c <= a by A199,YELLOW_0:59; hence thesis by AAA,A60,YELLOW_0:25; end; suppose f.x = c & f.y = b; then c <= b by A199,YELLOW_0:59; hence thesis by AAA,A63,YELLOW_0:25; end; suppose f.x = c & f.y = c; hence thesis by A124; end; suppose f.x = c & f.y = d; then c <= d by A199,YELLOW_0:59; hence thesis by AAA,A65,YELLOW_0:25; end; suppose A209: f.x = c & f.y = e; A210: dw c= t proof let X be object; assume X in dw; then X=0 or X=1 by CARD_1:50,TARSKI:def 2; hence thesis by CARD_1:51,ENUMSET1:def 1; end; f.t = e by A123; then A211: t = y by A124,A209; f.dw = c by A123; then dw=x by A124,A209; hence thesis by A210,A211,YELLOW_1:3; end; suppose A212: f.x = d & f.y = a; A213: a <= b by A59,YELLOW_0:25; d <= a by A199,A212,YELLOW_0:59; then d <= b by A213,ORDERS_2:3; hence thesis by AAA,A64,YELLOW_0:25; end; suppose f.x = d & f.y = b; then d <= b by A199,YELLOW_0:59; hence thesis by AAA,A64,YELLOW_0:25; end; suppose f.x = d & f.y = c; then d <= c by A199,YELLOW_0:59; hence thesis by AAA,A65,YELLOW_0:25; end; suppose f.x = d & f.y = d; hence thesis by A124; end; suppose A214: f.x = d & f.y = e; f.t = e by A123; then A215: t = y by A124,A214; f.tj = d by A123; then tj=x by A124,A214; hence thesis by A215,YELLOW_1:3; end; suppose A216: f.x = e & f.y = a; A217: b <= d by A64,YELLOW_0:25; A218: d <= e by A62,YELLOW_0:25; a <= b by A59,YELLOW_0:25; then a <= d by A217,ORDERS_2:3; then A219: a <= e by A218,ORDERS_2:3; e <= a by A199,A216,YELLOW_0:59; hence thesis by AAA,A219,ORDERS_2:2; end; suppose A220: f.x = e & f.y = b; A221: d <= e by A62,YELLOW_0:25; b <= d by A64,YELLOW_0:25; then A222: b <= e by A221,ORDERS_2:3; e <= b by A199,A220,YELLOW_0:59; hence thesis by AAA,A222,ORDERS_2:2; end; suppose f.x = e & f.y = c; then e <= c by A199,YELLOW_0:59; hence thesis by AAA,A61,YELLOW_0:25; end; suppose f.x = e & f.y = d; then e <= d by A199,YELLOW_0:59; hence thesis by AAA,A62,YELLOW_0:25; end; suppose f.x = e & f.y = e; hence thesis by A124; end; end; end; take f; f is one-to-one by A124; hence thesis by A68,A156,A157,WAYBEL_0:66; end; end; end; theorem Th10: for L being LATTICE holds (ex K being full Sublattice of L st M_3,K are_isomorphic) iff ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e & b"\/"d = e & c"\/"d = e proof set cn = the carrier of M_3; let L be LATTICE; A1: cn = {0, 1, 2 \ 1 , 3 \ 2, 3} by YELLOW_1:1; thus (ex K being full Sublattice of L st M_3,K are_isomorphic) implies ex a, b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c "/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e & b "\/"d = e & c"\/"d = e proof reconsider td = 3\2 as Element of M_3 by A1,ENUMSET1:def 3; reconsider dj = 2\1 as Element of M_3 by A1,ENUMSET1:def 3; reconsider t = 3 as Element of M_3 by A1,ENUMSET1:def 3; reconsider j = 1 as Element of M_3 by A1,ENUMSET1:def 3; reconsider cl = the carrier of L as non empty set; reconsider z = 0 as Element of M_3 by A1,ENUMSET1:def 3; given K being full Sublattice of L such that A2: M_3,K are_isomorphic; consider f being Function of M_3,K such that A3: f is isomorphic by A2; A4: K is non empty by A3,WAYBEL_0:def 38; then A5: f is one-to-one monotone by A3,WAYBEL_0:def 38; reconsider K as non empty SubRelStr of L by A3,WAYBEL_0:def 38; reconsider ck = the carrier of K as non empty set; A6: ck = rng f by A3,WAYBEL_0:66; reconsider g=f as Function of cn,ck; reconsider a=g.z,b=g.j,c =g.dj,d=g.td,e=g.t as Element of K; reconsider ck as non empty Subset of cl by YELLOW_0:def 13; A7: b in ck; A8: c in ck; A9: e in ck; A10: d in ck; a in ck; then reconsider A=a,B=b,C=c,D=d,E=e as Element of L by A7,A8,A10,A9; take A,B,C,D,E; thus A<>B by A5,WAYBEL_1:def 1; thus A<>C by A5,Th2,WAYBEL_1:def 1; thus A<>D by A5,Th4,WAYBEL_1:def 1; thus A<>E by A5,WAYBEL_1:def 1; now assume f.j = f.dj; then j = dj by A4,A5,WAYBEL_1:def 1; then 1 in 1 by Th2,TARSKI:def 1; hence contradiction; end; hence B<>C; now assume f.j = f.td; then A11: j = td by A4,A5,WAYBEL_1:def 1; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A11,Th4,TARSKI:def 1; end; hence B<>D; thus B<>E by A5,WAYBEL_1:def 1; now assume f.dj = f.td; then A12: dj = td by A4,A5,WAYBEL_1:def 1; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A12,Th4,TARSKI:def 1; end; hence C<>D; now assume f.dj = f.t; then A13: dj = t by A4,A5,WAYBEL_1:def 1; 0 in t by CARD_1:51,ENUMSET1:def 1; hence contradiction by A13,Th2,TARSKI:def 1; end; hence C<>E; now assume f.td = f.t; then A14: td = t by A4,A5,WAYBEL_1:def 1; 0 in t by CARD_1:51,ENUMSET1:def 1; hence contradiction by A14,Th4,TARSKI:def 1; end; hence D<>E; z c= j; then z <= j by YELLOW_1:3; then a <= b by A3,WAYBEL_0:66; then A <= B by YELLOW_0:59; hence A "/\" B = A by YELLOW_0:25; z c= dj; then z <= dj by YELLOW_1:3; then a <= c by A3,WAYBEL_0:66; then A <= C by YELLOW_0:59; hence A "/\" C = A by YELLOW_0:25; z c= td; then z <= td by YELLOW_1:3; then a <= d by A3,WAYBEL_0:66; then A <= D by YELLOW_0:59; hence A "/\" D = A by YELLOW_0:25; Segm 1 c= Segm 3 by NAT_1:39; then j <= t by YELLOW_1:3; then b <= e by A3,WAYBEL_0:66; then B <= E by YELLOW_0:59; hence B "/\" E = B by YELLOW_0:25; dj c= t proof let x be object; assume x in dj; then x=1 by Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; then dj <= t by YELLOW_1:3; then c <= e by A3,WAYBEL_0:66; then C <= E by YELLOW_0:59; hence C"/\"E = C by YELLOW_0:25; td <= t by YELLOW_1:3; then d <= e by A3,WAYBEL_0:66; then D <= E by YELLOW_0:59; hence D"/\"E = D by YELLOW_0:25; thus B"/\"C = A proof A15: now assume B"/\"C = D; then D <= C by YELLOW_0:23; then d <= c by YELLOW_0:60; then td <= dj by A3,WAYBEL_0:66; then A16: td c= dj by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A16,Th2,TARSKI:def 1; end; A17: now assume B"/\"C = B; then B <= C by YELLOW_0:25; then b <= c by YELLOW_0:60; then j <= dj by A3,WAYBEL_0:66; then A18: j c= dj by YELLOW_1:3; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A18,Th2,TARSKI:def 1; end; A19: now assume B"/\"C = E; then E <= C by YELLOW_0:23; then e <= c by YELLOW_0:60; then t <= dj by A3,WAYBEL_0:66; then A20: t c= dj by YELLOW_1:3; 2 in t by CARD_1:51,ENUMSET1:def 1; hence contradiction by A20,Th2,TARSKI:def 1; end; A21: now assume B"/\"C = C; then C <= B by YELLOW_0:25; then c <= b by YELLOW_0:60; then dj <= j by A3,WAYBEL_0:66; then A22: dj c= j by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A22,CARD_1:49,TARSKI:def 1; end; ex_inf_of {B,C},L by YELLOW_0:21; then inf{B,C} in the carrier of K by YELLOW_0:def 16; then B"/\"C in rng f by A6,YELLOW_0:40; then ex x being object st x in dom f & B"/\"C = f.x by FUNCT_1:def 3; hence thesis by A1,A17,A21,A15,A19,ENUMSET1:def 3; end; thus B"/\"D = A proof A23: now assume B"/\"D = D; then D <= B by YELLOW_0:23; then d <= b by YELLOW_0:60; then td <= j by A3,WAYBEL_0:66; then A24: td c= j by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A24,CARD_1:49,TARSKI:def 1; end; A25: now assume B"/\"D = C; then C <= B by YELLOW_0:23; then c <= b by YELLOW_0:60; then dj <= j by A3,WAYBEL_0:66; then A26: dj c= j by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A26,CARD_1:49,TARSKI:def 1; end; A27: now assume B"/\"D = B; then B <= D by YELLOW_0:25; then b <= d by YELLOW_0:60; then j <= td by A3,WAYBEL_0:66; then A28: j c= td by YELLOW_1:3; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A28,Th4,TARSKI:def 1; end; A29: now assume B"/\"D = E; then E <= B by YELLOW_0:23; then e <= b by YELLOW_0:60; then t <= j by A3,WAYBEL_0:66; then A30: t c= j by YELLOW_1:3; 2 in t by CARD_1:51,ENUMSET1:def 1; hence contradiction by A30,CARD_1:49,TARSKI:def 1; end; ex_inf_of {B,D},L by YELLOW_0:21; then inf{B,D} in the carrier of K by YELLOW_0:def 16; then B"/\"D in rng f by A6,YELLOW_0:40; then ex x being object st x in dom f & B"/\"D = f.x by FUNCT_1:def 3; hence thesis by A1,A27,A25,A23,A29,ENUMSET1:def 3; end; thus C"/\"D = A proof A31: now assume C"/\"D = D; then D <= C by YELLOW_0:23; then d <= c by YELLOW_0:60; then td <= dj by A3,WAYBEL_0:66; then A32: td c= dj by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A32,Th2,TARSKI:def 1; end; A33: now assume C"/\"D = E; then E <= C by YELLOW_0:23; then e <= c by YELLOW_0:60; then t <= dj by A3,WAYBEL_0:66; then A34: t c= dj by YELLOW_1:3; 2 in t by CARD_1:51,ENUMSET1:def 1; hence contradiction by A34,Th2,TARSKI:def 1; end; A35: now assume C"/\"D = C; then C <= D by YELLOW_0:25; then c <= d by YELLOW_0:60; then dj <= td by A3,WAYBEL_0:66; then A36: dj c= td by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A36,Th4,TARSKI:def 1; end; A37: now assume C"/\"D = B; then B <= C by YELLOW_0:23; then b <= c by YELLOW_0:60; then j <= dj by A3,WAYBEL_0:66; then A38: j c= dj by YELLOW_1:3; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A38,Th2,TARSKI:def 1; end; ex_inf_of {C,D},L by YELLOW_0:21; then inf{C,D} in the carrier of K by YELLOW_0:def 16; then C"/\"D in rng f by A6,YELLOW_0:40; then ex x being object st x in dom f & C"/\"D = f.x by FUNCT_1:def 3; hence thesis by A1,A37,A35,A31,A33,ENUMSET1:def 3; end; thus B"\/"C = E proof A39: now assume B"\/"C = C; then C >= B by YELLOW_0:24; then c >= b by YELLOW_0:60; then dj >= j by A3,WAYBEL_0:66; then A40: j c= dj by YELLOW_1:3; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A40,Th2,TARSKI:def 1; end; A41: now assume B"\/"C = B; then B >= C by YELLOW_0:24; then b >= c by YELLOW_0:60; then j >= dj by A3,WAYBEL_0:66; then A42: dj c= j by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A42,CARD_1:49,TARSKI:def 1; end; A43: now assume B"\/"C = D; then D >= C by YELLOW_0:22; then d >= c by YELLOW_0:60; then td >= dj by A3,WAYBEL_0:66; then A44: dj c= td by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A44,Th4,TARSKI:def 1; end; A45: now assume B"\/"C = A; then A >= C by YELLOW_0:22; then a >= c by YELLOW_0:60; then z >= dj by A3,WAYBEL_0:66; then dj c= z by YELLOW_1:3; hence contradiction by Th2; end; ex_sup_of {B,C},L by YELLOW_0:20; then sup{B,C} in the carrier of K by YELLOW_0:def 17; then B"\/"C in rng f by A6,YELLOW_0:41; then ex x being object st x in dom f & B"\/"C = f.x by FUNCT_1:def 3; hence thesis by A1,A41,A39,A43,A45,ENUMSET1:def 3; end; thus B"\/"D = E proof A46: now assume B"\/"D = D; then D >= B by YELLOW_0:22; then d >= b by YELLOW_0:60; then td >= j by A3,WAYBEL_0:66; then A47: j c= td by YELLOW_1:3; 0 in j by CARD_1:49,TARSKI:def 1; hence contradiction by A47,Th4,TARSKI:def 1; end; A48: now assume B"\/"D = B; then B >= D by YELLOW_0:22; then b >= d by YELLOW_0:60; then j >= td by A3,WAYBEL_0:66; then A49: td c= j by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A49,CARD_1:49,TARSKI:def 1; end; A50: now assume B"\/"D = C; then C >= D by YELLOW_0:22; then c >= d by YELLOW_0:60; then dj >= td by A3,WAYBEL_0:66; then A51: td c= dj by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A51,Th2,TARSKI:def 1; end; A52: now assume B"\/"D = A; then A >= B by YELLOW_0:22; then a >= b by YELLOW_0:60; then z >= j by A3,WAYBEL_0:66; then j c= z by YELLOW_1:3; hence contradiction; end; ex_sup_of {B,D},L by YELLOW_0:20; then sup{B,D} in the carrier of K by YELLOW_0:def 17; then B"\/"D in rng f by A6,YELLOW_0:41; then ex x being object st x in dom f & B"\/"D = f.x by FUNCT_1:def 3; hence thesis by A1,A48,A50,A46,A52,ENUMSET1:def 3; end; thus C"\/"D = E proof A53: now assume C"\/"D = B; then B >= C by YELLOW_0:22; then b >= c by YELLOW_0:60; then j >= dj by A3,WAYBEL_0:66; then A54: dj c= j by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; then 1 in 1 by A54; hence contradiction; end; A55: now assume C"\/"D = D; then D >= C by YELLOW_0:22; then d >= c by YELLOW_0:60; then td >= dj by A3,WAYBEL_0:66; then A56: dj c= td by YELLOW_1:3; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A56,Th4,TARSKI:def 1; end; A57: now assume C"\/"D = C; then C >= D by YELLOW_0:24; then c >= d by YELLOW_0:60; then dj >= td by A3,WAYBEL_0:66; then A58: td c= dj by YELLOW_1:3; 2 in td by Th4,TARSKI:def 1; hence contradiction by A58,Th2,TARSKI:def 1; end; A59: now assume C"\/"D = A; then A >= C by YELLOW_0:22; then a >= c by YELLOW_0:60; then z >= dj by A3,WAYBEL_0:66; then dj c= z by YELLOW_1:3; hence contradiction by Th2; end; ex_sup_of {C,D},L by YELLOW_0:20; then sup{C,D} in the carrier of K by YELLOW_0:def 17; then C"\/"D in rng f by A6,YELLOW_0:41; then ex x being object st x in dom f & C"\/"D = f.x by FUNCT_1:def 3; hence thesis by A1,A53,A57,A55,A59,ENUMSET1:def 3; end; end; thus (ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b "/\"e = b & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b "\/"c = e & b"\/"d = e & c"\/" d = e)) implies ex K being full Sublattice of L st M_3,K are_isomorphic proof given a,b,c,d,e being Element of L such that AAA: a,b,c,d,e are_mutually_distinct and A70: a"/\"b = a and A71: a"/\"c = a and A72: a"/\"d = a and A73: b"/\"e = b and A74: c"/\"e = c and A75: d"/\" e = d and A76: b"/\"c = a and A77: b"/\"d = a and A78: c"/\"d = a and A79: b"\/"c = e and A80: b"\/"d = e and A81: c"\/" d = e; set ck = {a,b,c,d,e}; reconsider ck as Subset of L; set K = subrelstr ck; A82: the carrier of K = ck by YELLOW_0:def 15; A83: K is meet-inheriting proof let x,y be Element of L; assume that A84: x in the carrier of K and A85: y in the carrier of K and ex_inf_of {x,y},L; per cases by A82,A84,A85,ENUMSET1:def 3; suppose x=a & y=a; then inf{x,y} = a"/\"a by YELLOW_0:40; then inf{x,y} = a by YELLOW_5:2; hence thesis by A82,ENUMSET1:def 3; end; suppose x=a & y=b; then inf{x,y} = a"/\"b by YELLOW_0:40; hence thesis by A70,A82,ENUMSET1:def 3; end; suppose x=a & y=c; then inf{x,y} = a"/\"c by YELLOW_0:40; hence thesis by A71,A82,ENUMSET1:def 3; end; suppose x=a & y=d; then inf{x,y} = a"/\"d by YELLOW_0:40; hence thesis by A72,A82,ENUMSET1:def 3; end; suppose A86: x=a & y=e; A87: c <= e by A74,YELLOW_0:25; a <= c by A71,YELLOW_0:25; then a <= e by A87,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then inf {x,y} = a by A86,YELLOW_0:40; hence thesis by A82,ENUMSET1:def 3; end; suppose x=b & y=a; then inf{x,y} = a"/\"b by YELLOW_0:40; hence thesis by A70,A82,ENUMSET1:def 3; end; suppose x=b & y=b; then inf{x,y} = b"/\"b by YELLOW_0:40; then inf{x,y} = b by YELLOW_5:2; hence thesis by A82,ENUMSET1:def 3; end; suppose x=b & y=c; then inf{x,y} = b"/\"c by YELLOW_0:40; hence thesis by A76,A82,ENUMSET1:def 3; end; suppose x=b & y=d; then inf{x,y} = b"/\"d by YELLOW_0:40; hence thesis by A77,A82,ENUMSET1:def 3; end; suppose x=b & y=e; then inf{x,y} = b"/\"e by YELLOW_0:40; hence thesis by A73,A82,ENUMSET1:def 3; end; suppose x=c & y=a; then inf{x,y} = a"/\"c by YELLOW_0:40; hence thesis by A71,A82,ENUMSET1:def 3; end; suppose x=c & y=b; then inf{x,y} = b"/\"c by YELLOW_0:40; hence thesis by A76,A82,ENUMSET1:def 3; end; suppose x=c & y=c; then inf{x,y} = c"/\"c by YELLOW_0:40; then inf{x,y} = c by YELLOW_5:2; hence thesis by A82,ENUMSET1:def 3; end; suppose x=c & y=d; then inf{x,y} = c"/\"d by YELLOW_0:40; hence thesis by A78,A82,ENUMSET1:def 3; end; suppose x=c & y=e; then inf{x,y} = c"/\"e by YELLOW_0:40; hence thesis by A74,A82,ENUMSET1:def 3; end; suppose x=d & y=a; then inf{x,y} = a"/\"d by YELLOW_0:40; hence thesis by A72,A82,ENUMSET1:def 3; end; suppose x=d & y=b; then inf{x,y} = b"/\"d by YELLOW_0:40; hence thesis by A77,A82,ENUMSET1:def 3; end; suppose x=d & y=c; then inf{x,y} = c"/\"d by YELLOW_0:40; hence thesis by A78,A82,ENUMSET1:def 3; end; suppose x=d & y=d; then inf{x,y} = d"/\"d by YELLOW_0:40; then inf{x,y} = d by YELLOW_5:2; hence thesis by A82,ENUMSET1:def 3; end; suppose x=d & y=e; then inf{x,y} = d"/\"e by YELLOW_0:40; hence thesis by A75,A82,ENUMSET1:def 3; end; suppose A88: x=e & y=a; A89: c <= e by A74,YELLOW_0:25; a <= c by A71,YELLOW_0:25; then a <= e by A89,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then inf {x,y} = a by A88,YELLOW_0:40; hence thesis by A82,ENUMSET1:def 3; end; suppose x=e & y=b; then inf{x,y} = b"/\"e by YELLOW_0:40; hence thesis by A73,A82,ENUMSET1:def 3; end; suppose x=e & y=c; then inf{x,y} = c"/\"e by YELLOW_0:40; hence thesis by A74,A82,ENUMSET1:def 3; end; suppose x=e & y=d; then inf{x,y} = d"/\"e by YELLOW_0:40; hence thesis by A75,A82,ENUMSET1:def 3; end; suppose x=e & y=e; then inf{x,y} = e"/\"e by YELLOW_0:40; then inf{x,y} = e by YELLOW_5:2; hence thesis by A82,ENUMSET1:def 3; end; end; K is join-inheriting proof let x,y be Element of L; assume that A90: x in the carrier of K and A91: y in the carrier of K and ex_sup_of {x,y},L; per cases by A82,A90,A91,ENUMSET1:def 3; suppose x=a & y=a; then sup{x,y} = a"\/"a by YELLOW_0:41; then sup{x,y} = a by YELLOW_5:1; hence thesis by A82,ENUMSET1:def 3; end; suppose x=a & y=b; then x"\/"y = b by A70,Th5; then sup{x,y} = b by YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=a & y=c; then x"\/"y = c by A71,Th5; then sup{x,y} = c by YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=a & y=d; then x"\/"y = d by A72,Th5; then sup{x,y} = d by YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A92: x=a & y=e; A93: c <= e by A74,YELLOW_0:25; a <= c by A71,YELLOW_0:25; then a <= e by A93,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then a"\/"e = e by Th5; then sup {x,y} = e by A92,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A94: x=b & y=a; a"\/"b = b by A70,Th5; then sup{x,y} = b by A94,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=b & y=b; then sup{x,y} = b"\/"b by YELLOW_0:41; then sup{x,y} = b by YELLOW_5:1; hence thesis by A82,ENUMSET1:def 3; end; suppose x=b & y=c; then sup{x,y} = b"\/"c by YELLOW_0:41; hence thesis by A79,A82,ENUMSET1:def 3; end; suppose x=b & y=d; then sup{x,y} = b"\/"d by YELLOW_0:41; hence thesis by A80,A82,ENUMSET1:def 3; end; suppose A95: x=b & y=e; b"\/"e = e by A73,Th5; then sup{x,y} = e by A95,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A96: x=c & y=a; c"\/"a = c by A71,Th5; then sup{x,y} = c by A96,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=c & y=b; then sup{x,y} = b"\/"c by YELLOW_0:41; hence thesis by A79,A82,ENUMSET1:def 3; end; suppose x=c & y=c; then sup{x,y} = c"\/"c by YELLOW_0:41; then sup{x,y} = c by YELLOW_5:1; hence thesis by A82,ENUMSET1:def 3; end; suppose x=c & y=d; then sup{x,y} = c"\/"d by YELLOW_0:41; hence thesis by A81,A82,ENUMSET1:def 3; end; suppose A97: x=c & y=e; c"\/"e = e by A74,Th5; then sup{x,y} = e by A97,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=d & y=a; then x"\/"y = d by A72,Th5; then sup{x,y} = d by YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=d & y=b; then sup{x,y} = b"\/"d by YELLOW_0:41; hence thesis by A80,A82,ENUMSET1:def 3; end; suppose x=d & y=c; then sup{x,y} = c"\/"d by YELLOW_0:41; hence thesis by A81,A82,ENUMSET1:def 3; end; suppose x=d & y=d; then sup{x,y} = d"\/"d by YELLOW_0:41; then sup{x,y} = d by YELLOW_5:1; hence thesis by A82,ENUMSET1:def 3; end; suppose A98: x=d & y=e; d"\/"e = e by A75,Th5; then sup{x,y} = e by A98,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A99: x=e & y=a; A100: c <= e by A74,YELLOW_0:25; a <= c by A71,YELLOW_0:25; then a <= e by A100,ORDERS_2:3; then a"/\"e = a by YELLOW_0:25; then a"\/"e = e by Th5; then sup {x,y} = e by A99,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A101: x=e & y=b; b"\/"e = e by A73,Th5; then sup{x,y} = e by A101,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A102: x=e & y=c; c"\/"e = e by A74,Th5; then sup{x,y} = e by A102,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose A103: x=e & y=d; d"\/"e = e by A75,Th5; then sup{x,y} = e by A103,YELLOW_0:41; hence thesis by A82,ENUMSET1:def 3; end; suppose x=e & y=e; then sup{x,y} = e"\/"e by YELLOW_0:41; then sup{x,y} = e by YELLOW_5:1; hence thesis by A82,ENUMSET1:def 3; end; end; then reconsider K as non empty full Sublattice of L by A83,YELLOW_0:def 15; take K; thus M_3,K are_isomorphic proof reconsider t = 3 as Element of M_3 by A1,ENUMSET1:def 3; reconsider td = 3\2 as Element of M_3 by A1,ENUMSET1:def 3; reconsider dj = 2\1 as Element of M_3 by A1,ENUMSET1:def 3; A104: now A105: 2 in t by CARD_1:51,ENUMSET1:def 1; assume dj=t; hence contradiction by A105,Th2,TARSKI:def 1; end; A106: now A107: 0 in t by CARD_1:51,ENUMSET1:def 1; assume td=t; hence contradiction by A107,Th4,TARSKI:def 1; end; reconsider j = 1 as Element of M_3 by A1,ENUMSET1:def 3; reconsider z = 0 as Element of M_3 by A1,ENUMSET1:def 3; defpred P[object,object] means for X being Element of M_3 st X=$1 holds ((X = z implies $2 = a) & (X = j implies $2 = b) & (X = dj implies $2 = c) & (X = td implies $2 = d) & (X = t implies $2 = e)); A108: now assume A109: j=dj; 1 in dj by Th2,TARSKI:def 1; hence contradiction by A109; end; A110: now assume A111: j=td; 2 in td by Th4,TARSKI:def 1; hence contradiction by A111,CARD_1:49,TARSKI:def 1; end; A112: now assume A113: dj=td; 2 in td by Th4,TARSKI:def 1; hence contradiction by A113,Th2,TARSKI:def 1; end; A114: for x being object st x in cn ex y being object st y in ck & P[x,y] proof let x be object; assume A115: x in cn; per cases by A1,A115,ENUMSET1:def 3; suppose A116: x = 0; take y=a; thus y in ck by ENUMSET1:def 3; let X be Element of M_3; thus thesis by A116,Th2,Th4; end; suppose A117: x=1; take y=b; thus y in ck by ENUMSET1:def 3; let X be Element of M_3; thus thesis by A108,A110,A117; end; suppose A118: x = 2\1; take y=c; thus y in ck by ENUMSET1:def 3; let X be Element of M_3; thus thesis by A108,A112,A104,A118,Th2; end; suppose A119: x = 3 \ 2; take y=d; thus y in ck by ENUMSET1:def 3; let X be Element of M_3; thus thesis by A110,A112,A106,A119,Th4; end; suppose A120: x = 3; take y=e; thus y in ck by ENUMSET1:def 3; let X be Element of M_3; thus thesis by A104,A106,A120; end; end; consider f being Function of cn,ck such that A121: for x being object st x in cn holds P[x,f.x] from FUNCT_2:sch 1( A114); reconsider f as Function of M_3,K by A82; A122: now let x,y be Element of M_3; assume A123: f.x = f.y; thus x=y proof per cases by A1,ENUMSET1:def 3; suppose x = z & y = z; hence thesis; end; suppose x = j & y = j; hence thesis; end; suppose x = dj & y = dj; hence thesis; end; suppose x = td & y = td; hence thesis; end; suppose x = t & y = t; hence thesis; end; suppose A124: x = z & y = j; then f.x=a by A121; hence thesis by AAA,A121,A123,A124; end; suppose A125: x = z & y = dj; then f.x=a by A121; hence thesis by AAA,A121,A123,A125; end; suppose A126: x = z & y = td; then f.x=a by A121; hence thesis by AAA,A121,A123,A126; end; suppose A127: x = z & y = t; then f.x=a by A121; hence thesis by AAA,A121,A123,A127; end; suppose A128: x = j & y = z; then f.x=b by A121; hence thesis by AAA,A121,A123,A128; end; suppose A129: x = j & y = dj; then f.x=b by A121; hence thesis by AAA,A121,A123,A129; end; suppose A130: x = j & y = td; then f.x=b by A121; hence thesis by AAA,A121,A123,A130; end; suppose A131: x = j & y = t; then f.x=b by A121; hence thesis by AAA,A121,A123,A131; end; suppose A132: x = dj & y = z; then f.x=c by A121; hence thesis by AAA,A121,A123,A132; end; suppose A133: x = dj & y = j; then f.x=c by A121; hence thesis by AAA,A121,A123,A133; end; suppose A134: x = dj & y = td; then f.x=c by A121; hence thesis by AAA,A121,A123,A134; end; suppose A135: x = dj & y = t; then f.x=c by A121; hence thesis by AAA,A121,A123,A135; end; suppose A136: x = td & y = z; then f.x=d by A121; hence thesis by AAA,A121,A123,A136; end; suppose A137: x = td & y = j; then f.x=d by A121; hence thesis by AAA,A121,A123,A137; end; suppose A138: x = td & y = dj; then f.x=d by A121; hence thesis by AAA,A121,A123,A138; end; suppose A139: x = td & y = t; then f.x=d by A121; hence thesis by AAA,A121,A123,A139; end; suppose A140: x = t & y = z; then f.x=e by A121; hence thesis by AAA,A121,A123,A140; end; suppose A141: x = t & y = j; then f.x=e by A121; hence thesis by AAA,A121,A123,A141; end; suppose A142: x = t & y = dj; then f.x=e by A121; hence thesis by AAA,A121,A123,A142; end; suppose A143: x = t & y = td; then f.x=e by A121; hence thesis by AAA,A121,A123,A143; end; end; end; A144: rng f c= ck proof let y be object; assume y in rng f; then consider x being object such that A145: x in dom f and A146: y=f.x by FUNCT_1:def 3; reconsider x as Element of M_3 by A145; x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:def 3; then y=a or y=d or y=c or y=b or y=e by A121,A146; hence thesis by ENUMSET1:def 3; end; A147: dom f = the carrier of M_3 by FUNCT_2:def 1; ck c= rng f proof let y be object; assume A148: y in ck; per cases by A148,ENUMSET1:def 3; suppose A149: y=a; a = f.z by A121; hence thesis by A147,A149,FUNCT_1:def 3; end; suppose A150: y=b; b=f.j by A121; hence thesis by A147,A150,FUNCT_1:def 3; end; suppose A151: y=c; c = f.dj by A121; hence thesis by A147,A151,FUNCT_1:def 3; end; suppose A152: y=d; d=f.td by A121; hence thesis by A147,A152,FUNCT_1:def 3; end; suppose A153: y=e; e=f.t by A121; hence thesis by A147,A153,FUNCT_1:def 3; end; end; then A154: rng f = ck by A144; A155: for x,y being Element of M_3 holds x <= y iff f.x <= f.y proof let x,y be Element of M_3; thus x <= y implies f.x <= f.y proof assume A156: x <= y; per cases by A1,ENUMSET1:def 3; suppose x=z & y=z; hence thesis; end; suppose A157: x=z & y=j; then A158: f.y = b by A121; A159: a <= b by A70,YELLOW_0:25; f.x = a by A121,A157; hence thesis by A158,A159,YELLOW_0:60; end; suppose A160: x=z & y=dj; then A161: f.y = c by A121; A162: a <= c by A71,YELLOW_0:25; f.x = a by A121,A160; hence thesis by A161,A162,YELLOW_0:60; end; suppose A163: x=z & y=td; then A164: f.y = d by A121; A165: a <= d by A72,YELLOW_0:25; f.x = a by A121,A163; hence thesis by A164,A165,YELLOW_0:60; end; suppose A166: x=z & y=t; A167: c <= e by A74,YELLOW_0:25; a <= c by A71,YELLOW_0:25; then A168: a <= e by A167,ORDERS_2:3; A169: f.y = e by A121,A166; f.x = a by A121,A166; hence thesis by A169,A168,YELLOW_0:60; end; suppose x=j & y=z; then j c= z by A156,YELLOW_1:3; hence thesis; end; suppose x=j & y=j; hence thesis; end; suppose A170: x=j & y=dj; 0 in j by CARD_1:49,TARSKI:def 1; then not j c= dj by Th2,TARSKI:def 1; hence thesis by A156,A170,YELLOW_1:3; end; suppose A171: x=j & y=td; 0 in j by CARD_1:49,TARSKI:def 1; then not j c= td by Th4,TARSKI:def 1; hence thesis by A156,A171,YELLOW_1:3; end; suppose A172: x=j & y=t; then A173: f.y = e by A121; A174: b <= e by A73,YELLOW_0:25; f.x = b by A121,A172; hence thesis by A173,A174,YELLOW_0:60; end; suppose x=dj & y=z; then dj c= z by A156,YELLOW_1:3; hence thesis by Th2; end; suppose A175: x=dj & y=j; A176: not 1 in j; 1 in dj by Th2,TARSKI:def 1; then not dj c= j by A176; hence thesis by A156,A175,YELLOW_1:3; end; suppose x=dj & y=dj; hence thesis; end; suppose A177: x=dj & y=td; 1 in dj by Th2,TARSKI:def 1; then not dj c= td by Th4,TARSKI:def 1; hence thesis by A156,A177,YELLOW_1:3; end; suppose A178: x=dj & y=t; then A179: f.y = e by A121; A180: c <= e by A74,YELLOW_0:25; f.x = c by A121,A178; hence thesis by A179,A180,YELLOW_0:60; end; suppose x=td & y=z; then td c= z by A156,YELLOW_1:3; hence thesis by Th4; end; suppose A181: x=td & y=j; 2 in td by Th4,TARSKI:def 1; then not td c= j by CARD_1:49,TARSKI:def 1; hence thesis by A156,A181,YELLOW_1:3; end; suppose A182: x=td & y=dj; 2 in td by Th4,TARSKI:def 1; then not td c= dj by Th2,TARSKI:def 1; hence thesis by A156,A182,YELLOW_1:3; end; suppose x=td & y=td; hence thesis; end; suppose A183: x=td & y=t; then A184: f.y = e by A121; A185: d <= e by A75,YELLOW_0:25; f.x = d by A121,A183; hence thesis by A184,A185,YELLOW_0:60; end; suppose x=t & y=z; then t c= z by A156,YELLOW_1:3; hence thesis; end; suppose A186: x=t & y=j; A187: not 1 in j; 1 in t by CARD_1:51,ENUMSET1:def 1; then not t c= j by A187; hence thesis by A156,A186,YELLOW_1:3; end; suppose A188: x=t & y=dj; 2 in t by CARD_1:51,ENUMSET1:def 1; then not t c= dj by Th2,TARSKI:def 1; hence thesis by A156,A188,YELLOW_1:3; end; suppose A189: x=t & y=td; 0 in t by CARD_1:51,ENUMSET1:def 1; then not t c= td by Th4,TARSKI:def 1; hence thesis by A156,A189,YELLOW_1:3; end; suppose x=t & y=t; hence thesis; end; end; thus f.x <= f.y implies x <= y proof A190: dj c= t proof let X be object; assume X in dj; then X=1 by Th2,TARSKI:def 1; hence thesis by CARD_1:51,ENUMSET1:def 1; end; A191: f.y in ck by A147,A154,FUNCT_1:def 3; A192: f.x in ck by A147,A154,FUNCT_1:def 3; assume A193: f.x <= f.y; per cases by A192,A191,ENUMSET1:def 3; suppose f.x = a & f.y = a; hence thesis by A122; end; suppose A194: f.x = a & f.y = b; f.z = a by A121; then z=x by A122,A194; then x c= y; hence thesis by YELLOW_1:3; end; suppose A195: f.x = a & f.y = c; f.z = a by A121; then z=x by A122,A195; then x c= y; hence thesis by YELLOW_1:3; end; suppose A196: f.x = a & f.y = d; f.z = a by A121; then z=x by A122,A196; then x c= y; hence thesis by YELLOW_1:3; end; suppose A197: f.x = a & f.y = e; f.z = a by A121; then z=x by A122,A197; then x c= y; hence thesis by YELLOW_1:3; end; suppose f.x = b & f.y = a; then b <= a by A193,YELLOW_0:59; hence thesis by AAA,A70,YELLOW_0:25; end; suppose f.x = b & f.y = b; hence thesis by A122; end; suppose f.x = b & f.y = c; then b <= c by A193,YELLOW_0:59; hence thesis by AAA,A76,YELLOW_0:25; end; suppose f.x = b & f.y = d; then b <= d by A193,YELLOW_0:59; hence thesis by AAA,A77,YELLOW_0:25; end; suppose A198: f.x = b & f.y = e; f.t = e by A121; then A199: t = y by A122,A198; f.j = b by A121; then A200: j=x by A122,A198; Segm 1 c= Segm 3 by NAT_1:39; hence thesis by YELLOW_1:3,A200,A199; end; suppose f.x = c & f.y = a; then c <= a by A193,YELLOW_0:59; hence thesis by AAA,A71,YELLOW_0:25; end; suppose f.x = c & f.y = b; then c <= b by A193,YELLOW_0:59; hence thesis by AAA,A76,YELLOW_0:25; end; suppose f.x = c & f.y = c; hence thesis by A122; end; suppose f.x = c & f.y = d; then c <= d by A193,YELLOW_0:59; hence thesis by AAA,A78,YELLOW_0:25; end; suppose A201: f.x = c & f.y = e; f.t = e by A121; then A202: t = y by A122,A201; f.dj = c by A121; then dj = x by A122,A201; hence thesis by A190,A202,YELLOW_1:3; end; suppose f.x = d & f.y = a; then d <= a by A193,YELLOW_0:59; hence thesis by AAA,A72,YELLOW_0:25; end; suppose f.x = d & f.y = b; then d <= b by A193,YELLOW_0:59; hence thesis by AAA,A77,YELLOW_0:25; end; suppose f.x = d & f.y = c; then d <= c by A193,YELLOW_0:59; hence thesis by AAA,A78,YELLOW_0:25; end; suppose f.x = d & f.y = d; hence thesis by A122; end; suppose A203: f.x = d & f.y = e; f.t = e by A121; then A204: t = y by A122,A203; f.td = d by A121; then td=x by A122,A203; hence thesis by A204,YELLOW_1:3; end; suppose A205: f.x = e & f.y = a; A206: a <= b by A70,YELLOW_0:25; e <= a by A193,A205,YELLOW_0:59; then e <= b by A206,ORDERS_2:3; hence thesis by AAA,A73,YELLOW_0:25; end; suppose f.x = e & f.y = b; then e <= b by A193,YELLOW_0:59; hence thesis by AAA,A73,YELLOW_0:25; end; suppose f.x = e & f.y = c; then e <= c by A193,YELLOW_0:59; hence thesis by AAA,A74,YELLOW_0:25; end; suppose f.x = e & f.y = d; then e <= d by A193,YELLOW_0:59; hence thesis by AAA,A75,YELLOW_0:25; end; suppose f.x = e & f.y = e; hence thesis by A122; end; end; end; take f; f is one-to-one by A122; hence thesis by A82,A154,A155,WAYBEL_0:66; end; end; end; begin:: Modular lattices definition let L be non empty RelStr; attr L is modular means for a,b,c being Element of L st a <= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c; end; registration cluster distributive -> modular for non empty antisymmetric reflexive with_infima RelStr; coherence proof let L be non empty antisymmetric reflexive with_infima RelStr; assume A1: L is distributive; now let a,b,c be Element of L; assume a <= c; hence a"\/"(b"/\"c) = (a"/\"c)"\/"(b"/\"c) by YELLOW_0:25 .= (a"\/"b)"/\"c by A1; end; hence thesis; end; end; Lm2: for L being LATTICE holds L is modular iff not ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e) proof let L be LATTICE; now given a,b,c,d,e being Element of L such that A1: b<>d and A2: a"/\"b = a and A3: d"/\"e = d and A4: b"/\"d = b and A5: c"/\"d = a and A6: b"\/"c = e; A7: b <= d by A4,YELLOW_0:23; b"\/"(c"/\"d) = b by A2,A5,Th5; hence not L is modular by A1,A3,A6,A7; end; hence L is modular implies not ex a,b,c,d,e being Element of L st ( a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e); now assume not L is modular; then consider x,y,z being Element of L such that A8: x <= z and A9: x"\/"(y"/\"z) <> (x"\/"y)"/\"z; x"\/"(y"/\"z) <= z"\/"(y"/\"z) by A8,YELLOW_5:7; then A10: x"\/"(y"/\"z) <= z by LATTICE3:17; set z1=(x"\/"y)"/\"z; set y1=y; (x"\/"y) <= (x"\/"y); then (x"\/"y)"/\"x <= (x"\/"y)"/\"z by A8,YELLOW_3:2; then x <= (x"\/"y)"/\"z by LATTICE3:18; then A11: x"\/"y <= z1"\/"y1 by YELLOW_5:7; set x1=x"\/"(y"/\"z); A12: y"/\"z <= y1 by YELLOW_0:23; y <= y; then A13: x1"/\"y1 <= y"/\"z by A10,YELLOW_3:2; set t=x"\/"y; set b=y"/\"z; A14: now assume A15: b=t; then (x"\/"y)"/\"z = y"/\"(z"/\"z) by LATTICE3:16 .= x"\/"y by A15,YELLOW_5:2 .= (x"\/"x)"\/"y by YELLOW_5:1 .= x"\/"(y"/\"z) by A15,LATTICE3:14; hence contradiction by A9; end; y"/\"z <= x1 by YELLOW_0:22; then (y"/\"z)"/\"(y"/\"z) <= x1"/\"y1 by A12,YELLOW_3:2; then A16: y"/\"z <= x1"/\"y1 by YELLOW_5:2; A17: z1 <= x"\/"y by YELLOW_0:23; thus ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d "/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e proof take b,x1,y1,z1,t; A18: y1 <= x"\/"y by YELLOW_0:22; now A19: y"/\"z <= y by YELLOW_0:23; assume A20: b=x1; then x <= y"/\"z by YELLOW_0:22; then x <= y by A19,YELLOW_0:def 2; hence contradiction by A9,A20,YELLOW_5:8; end; hence b<>x1; now assume A21: b=y1; then y <= z by YELLOW_0:23; hence contradiction by A8,A9,A21,YELLOW_5:9,10; end; hence b<>y1; now assume b=z1; then A22: (x"\/"y)"/\"z <= x"\/"(y"/\"z) by YELLOW_0:22; x"\/"(y"/\"z) <= (x"\/"y)"/\"z by A8,Th8; hence contradiction by A9,A22,YELLOW_0:def 3; end; hence b<>z1; thus b<>t by A14; now A23: x1"\/"y1 = x "\/" ((y"/\"z)"\/"y) by LATTICE3:14 .= t by LATTICE3:17; assume A24: x1=y1; then A25: x1"\/"y1 = x1 by YELLOW_5:1; x1"/\"y1 = x1 by A24,YELLOW_5:2; hence contradiction by A16,A13,A14,A25,A23,YELLOW_0:def 3; end; hence x1<>y1; thus x1<>z1 by A9; now assume t=x1; then A26: (x"\/"y)"/\"z <= x"\/"(y"/\"z) by YELLOW_0:23; x"\/"(y"/\"z) <= (x"\/"y)"/\"z by A8,Th8; hence contradiction by A9,A26,YELLOW_0:def 3; end; hence x1<>t; now A27: y1"/\"z1 = ((x"\/"y)"/\"y)"/\"z by LATTICE3:16 .= b by LATTICE3:18; assume A28: y1=z1; then A29: z1"\/"y1 = z1 by YELLOW_5:1; z1"/\"y1 = z1 by A28,YELLOW_5:2; hence contradiction by A14,A17,A11,A29,A27,YELLOW_0:def 3; end; hence y1<>z1; now assume A30: y1=t; then x <= y by YELLOW_0:22; then x "/\" x <= y"/\"z by A8,YELLOW_3:2; then x <= y"/\"z by YELLOW_5:2; hence contradiction by A9,A30,YELLOW_5:8; end; hence y1<>t; now A31: y <= x"\/"y by YELLOW_0:22; assume A32: z1=t; then x"\/"y <= z by YELLOW_0:23; then y <= z by A31,YELLOW_0:def 2; hence contradiction by A9,A32,YELLOW_5:10; end; hence z1<>t; b <= x1 by YELLOW_0:22; hence b"/\"x1 = b by YELLOW_5:10; b <= y1 by YELLOW_0:23; hence b"/\"y1 = b by YELLOW_5:10; y1 <= t by YELLOW_0:22; hence y1"/\"t = y1 by YELLOW_5:10; z1 <= t by YELLOW_0:23; hence z1"/\"t = z1 by YELLOW_5:10; thus x1"/\"y1 = b by A16,A13,YELLOW_0:def 3; thus x1"/\"z1 = x1 by A8,Th8,YELLOW_5:10; thus y1"/\"z1 = y"/\"(x"\/"y)"/\"z by LATTICE3:16 .= b by LATTICE3:18; thus x1"\/"y1 = x "\/" ((y"/\"z)"\/"y) by LATTICE3:14 .= t by LATTICE3:17; (x"\/"y) <= (x"\/"y); then (x"\/"y)"/\"x <= (x"\/"y)"/\"z by A8,YELLOW_3:2; then x <= (x"\/"y)"/\"z by LATTICE3:18; then A33: x"\/"y <= z1"\/"y1 by YELLOW_5:7; z1 <= x"\/"y by YELLOW_0:23; then y1"\/"z1 <= x"\/"y by A18,YELLOW_5:9; hence thesis by A33,YELLOW_0:def 3; end; end; hence thesis; end; theorem for L being LATTICE holds L is modular iff not ex K being full Sublattice of L st N_5,K are_isomorphic proof let L be LATTICE; thus L is modular implies not ex K being full Sublattice of L st N_5,K are_isomorphic proof assume L is modular; then not ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e) by Lm2; hence thesis by Th9; end; assume not ex K being full Sublattice of L st N_5,K are_isomorphic; then not ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & c"/\"e = c & d "/\"e = d & b"/\"c = a & b"/\"d = b & c"/\"d = a & b"\/"c = e & c"\/"d = e) by Th9; hence thesis by Lm2; end; Lm3: for L being LATTICE st L is modular holds L is distributive iff not ex a, b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c "/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e & b "\/"d = e & c"\/"d = e) proof let L be LATTICE; assume A1: L is modular; now given a,b,c,d,e being Element of L such that A2: a<>d and A3: d"/\" e = d and A4: b"/\"c = a and A5: b"/\"d = a and A6: c"/\"d = a and A7: b"\/"c = e; (b"/\"c)"\/"(b"/\"d) = a by A4,A5,YELLOW_5:1; hence not L is distributive by A2,A3,A4,A6,A7; end; hence L is distributive implies not ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a "/\"c = a & a"/\"d = a & b"/\"e = b & c"/\"e = c & d"/\" e = d & b"/\"c = a & b "/\"d = a & c"/\"d = a & b"\/"c = e & b"\/"d = e & c"\/"d = e; now assume not L is distributive; then consider x,y,z being Element of L such that A8: x"/\"(y"\/"z) <> (x"/\"y)"\/"(x"/\"z); set t=(x"\/"y)"/\"(y"\/"z)"/\"(z"\/"x); set b=(x"/\"y)"\/"(y"/\"z)"\/"(z"/\"x); A9: x"/\"y <= x by YELLOW_0:23; A10: x "/\" t = (x"/\"((x"\/"y)"/\"(y"\/"z)))"/\"(z"\/"x) by LATTICE3:16 .= ((x"/\"(x"\/"y)"/\"(y"\/"z)))"/\"(z"\/"x) by LATTICE3:16 .= x"/\"(y"\/"z)"/\"(z"\/"x) by LATTICE3:18 .= (x"/\"(z"\/"x))"/\"(y"\/"z) by LATTICE3:16 .= x"/\"(y"\/"z) by LATTICE3:18; A11: x <= x; (y"/\"z) <= z by YELLOW_0:23; then A12: ((y"/\"z)"/\"x) "\/" (z"/\"x) = z"/\"x by A11,YELLOW_3:2,YELLOW_5:8; A13: z"/\"x <= x by YELLOW_0:23; A14: now assume b=t; then x"/\"(y"\/"z) = ((x"/\"y)"\/"((y"/\"z)"\/"(z"/\"x)))"/\" x by A10, LATTICE3:14 .= (x"/\"y)"\/"(((y"/\"z)"\/"(z"/\"x))"/\"x) by A1,A9 .= (x"/\"y)"\/"(z"/\"x) by A1,A13,A12; hence contradiction by A8; end; set y1=(y"\/"b)"/\"t; A15: (y"/\"z) <= (y"\/"z) by YELLOW_5:5; (y"/\"z) <= (x"\/"y) by YELLOW_5:5; then (y"/\"z) "/\" (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) by A15,YELLOW_3:2; then A16: (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2; (y"/\"z) <= (z"\/" x) by YELLOW_5:5; then (y"/\"z) "/\" (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/" x) by A16 ,YELLOW_3:2; then A17: (y"/\"z) <= t by YELLOW_5:2; A18: x"/\"t = (x "/\"((x"\/"y)"/\"(y"\/"z)))"/\"(z"\/"x) by LATTICE3:16 .= ((x "/\"(x"\/"y))"/\"(y"\/"z))"/\"(z"\/"x) by LATTICE3:16 .= (x "/\"(y"\/"z))"/\"(z"\/"x) by LATTICE3:18 .= ((z"\/"x)"/\"x)"/\"(y"\/"z) by LATTICE3:16 .= x "/\"(y"\/"z) by LATTICE3:18; set z1=(z"\/"b)"/\"t; A19: (z"/\"x) <= (y"\/"z) by YELLOW_5:5; (z"/\"x) <= (x"\/"y) by YELLOW_5:5; then (z"/\"x) "/\" (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) by A19,YELLOW_3:2; then A20: (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2; (z"/\"x) <= (z"\/" x) by YELLOW_5:5; then (z"/\"x) "/\" (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/" x) by A20 ,YELLOW_3:2; then A21: (z"/\"x) <= t by YELLOW_5:2; A22: y"/\"t = (y "/\"((x"\/"y)"/\"(y"\/"z)))"/\"(z"\/"x) by LATTICE3:16 .= ((y "/\"(x"\/"y))"/\"(y"\/"z))"/\"(z"\/"x) by LATTICE3:16 .= (y "/\"(y"\/"z))"/\"(z"\/"x) by LATTICE3:18 .= y "/\"(x"\/"z) by LATTICE3:18; A23: x <= x"\/"(y"/\"z) by YELLOW_0:22; x"/\"z <= x by YELLOW_0:23; then A24: x"/\"z <= x"\/"(y"/\"z) by A23,YELLOW_0:def 2; A25: y <= y"\/"z by YELLOW_0:22; A26: z"\/"(x"/\"y) <= (z"\/"x) "/\" ( z "\/"y) by Th7; A27: y"\/"(x"/\"z) <= (y"\/"x) "/\" ( y "\/"z) by Th7; A28: x <= x"\/"y by YELLOW_0:22; x"/\"(z"\/"y) <= x by YELLOW_0:23; then A29: x"/\"(z"\/"y) <= x"\/"y by A28,YELLOW_0:def 2; A30: y"\/"b = (y "\/"((x"/\"y)"\/"(y"/\"z)))"\/"(z"/\"x) by LATTICE3:14 .= ((y "\/"(x"/\"y))"\/"(y"/\"z))"\/"(z"/\"x) by LATTICE3:14 .= (y "\/"(y"/\"z))"\/"(z"/\"x) by LATTICE3:17 .= y "\/"(x"/\"z) by LATTICE3:17; A31: x <= x"\/"(z"/\"y) by YELLOW_0:22; x"/\"y <= x by YELLOW_0:23; then A32: x"/\"y <= x"\/"(z"/\"y) by A31,YELLOW_0:def 2; A33: z <= z"\/"y by YELLOW_0:22; A34: y"\/"(z"/\"x) <= (y"\/"z) "/\" ( y "\/"x) by Th7; A35: (x"/\"y)"\/"(y"/\"z) <= y "/\" ( x "\/"z) by Th6; A36: y"/\"z <= y by YELLOW_0:23; A37: z <= z"\/"x by YELLOW_0:22; z"/\"(y"\/"x) <= z by YELLOW_0:23; then A38: z"/\"(y"\/"x) <= z"\/"x by A37,YELLOW_0:def 2; A39: z"\/"b = (z "\/"(z"/\"x))"\/"((x"/\"y)"\/"(y"/\"z)) by LATTICE3:14 .= z"\/"((y"/\"z)"\/"(x"/\"y)) by LATTICE3:17 .= (z"\/"(y"/\"z))"\/"(x"/\"y) by LATTICE3:14 .= z"\/"(x"/\"y) by LATTICE3:17; (x"/\"y)"\/"(x"/\"z) <= x"/\"(y"\/"z) by Th6; then ((x"/\"y)"\/"(x"/\"z))"\/"((x"/\"y)"\/"(y"/\"z)) <= (x"/\"(y"\/"z) ) "\/" (y"/\"(x"\/"z)) by A35,YELLOW_3:3; then (x"/\"z)"\/"((x"/\"y)"\/"((x"/\"y)"\/"(y"/\"z))) <= (x"/\"(y"\/"z) ) "\/" (y"/\"(x"\/"z)) by LATTICE3:14; then (x"/\"z)"\/"(((x"/\"y)"\/"(x"/\"y))"\/"(y"/\"z)) <= (x"/\"(y"\/"z) ) "\/" (y"/\"(x"\/"z)) by LATTICE3:14; then (x"/\"y)"\/"(x"/\"y)"\/"(x"/\"z)"\/"(y"/\"z) <= (x"/\"(y"\/"z)) "\/" (y "/\"(x"\/"z)) by LATTICE3:14; then (x"/\"y)"\/"(x"/\"z)"\/"(y"/\"z) <= (x"/\"(y"\/"z)) "\/" (y"/\"(x "\/" z)) by YELLOW_5:1; then A40: b <= (x"/\"t)"\/"(y"/\"t) by A18,A22,LATTICE3:14; z1 <= t by YELLOW_0:23; then A41: t "/\" z1 = z1 by YELLOW_5:10; A42: z <= z"\/"(y"/\"x) by YELLOW_0:22; z"/\"x <= z by YELLOW_0:23; then A43: z"/\"x <= z"\/"(y"/\"x) by A42,YELLOW_0:def 2; A44: y <= y"\/"x by YELLOW_0:22; A45: x <= x"\/"z by YELLOW_0:22; x"/\"(y"\/"z) <= x by YELLOW_0:23; then A46: x"/\"(y"\/"z) <= x"\/"z by A45,YELLOW_0:def 2; A47: x"\/"b = (x"\/"((x"/\"y)"\/"(y"/\"z)))"\/"(z"/\"x) by LATTICE3:14 .= ((x"\/"(x"/\"y))"\/"(y"/\"z))"\/"(z"/\"x) by LATTICE3:14 .= (x "\/"(y"/\"z))"\/"(z"/\"x) by LATTICE3:17 .= ((z"/\"x)"\/"x) "\/"(y"/\"z) by LATTICE3:14 .= x "\/"(y"/\"z) by LATTICE3:17; z"\/"(y"/\"x) <= (z"\/"y)"/\"(z"\/"x) by Th7; then (z"\/"(y"/\"x))"/\"(y"\/"(z"/\"x)) <= ((z"\/"y)"/\"(z"\/"x))"/\"(( y "\/" z)"/\"(y"\/"x)) by A34,YELLOW_3:2; then (z"\/"b)"/\"(y"\/"b) <= ((z"\/"x)"/\"(z"\/"y))"/\"(z"\/"y)"/\"(y"\/"x ) by A30,A39,LATTICE3:16; then (z"\/"b)"/\"(y"\/"b) <= (z"\/"x)"/\"((z"\/"y)"/\"(z"\/"y))"/\"(y "\/" x) by LATTICE3:16; then (z"\/"b)"/\"(y"\/"b) <= (z"\/"x)"/\"(z"\/"y)"/\"(y"\/"x) by YELLOW_5:2 ; then A48: (z"\/"b)"/\"(y"\/"b) <= t by LATTICE3:16; y1 <= t by YELLOW_0:23; then A49: t "/\" y1 = y1 by YELLOW_5:10; set x1=(x"\/"b)"/\"t; A50: (x"/\"y) <= (y"\/"z) by YELLOW_5:5; (x"/\"y) <= (x"\/"y) by YELLOW_5:5; then (x"/\"y) "/\" (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) by A50,YELLOW_3:2; then A51: (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2; A52: z"/\"t = (z "/\"(z"\/"x))"/\"((x"\/"y)"/\"(y"\/"z)) by LATTICE3:16 .= z"/\"((y"\/"z)"/\"(x"\/"y)) by LATTICE3:18 .= (z"/\"(y"\/"z))"/\"(x"\/"y) by LATTICE3:16 .= z"/\"(x"\/"y) by LATTICE3:18; x"\/"(y"/\"z) <= (x"\/"y)"/\"(x"\/"z) by Th7; then (x"\/"(y"/\"z))"/\"(y"\/"(x"/\"z)) <= ((x"\/"y)"/\"(x"\/"z))"/\"(( y "\/" x)"/\"(y"\/"z)) by A27,YELLOW_3:2; then (x"\/"b)"/\"(y"\/"b) <= ((x"\/"z)"/\"(x"\/"y))"/\"(x"\/"y)"/\"(y"\/"z ) by A47,A30,LATTICE3:16; then (x"\/"b)"/\"(y"\/"b) <= (x"\/"z)"/\"((x"\/"y)"/\"(x"\/"y))"/\"(y "\/" z) by LATTICE3:16; then (x"\/"b)"/\"(y"\/"b) <= (x"\/"z)"/\"(x"\/"y)"/\"(y"\/"z) by YELLOW_5:2 ; then A53: (x"\/"b)"/\"(y"\/"b) <= t by LATTICE3:16; A54: (z"/\"y)"\/"(y"/\"x) <= y "/\" ( z "\/"x) by Th6; A55: y"/\"x <= y by YELLOW_0:23; A56: x1 "/\" y1 = (x"\/"b)"/\"(t "/\" ((y"\/"b)"/\"t)) by LATTICE3:16 .= (x"\/"b)"/\"(t "/\" t "/\" (y"\/"b)) by LATTICE3:16 .= (x"\/"b)"/\"((y"\/"b) "/\" t) by YELLOW_5:2 .= (x"\/"b)"/\"(y"\/"b) "/\" t by LATTICE3:16 .= (x "\/"(y"/\"z))"/\"(y "\/"(x"/\"z)) by A47,A30,A53,YELLOW_5:10 .= (y"/\"(x "\/"(y"/\"z))) "\/"(x"/\"z) by A1,A24 .= b by A1,A36; then b <= y1 by YELLOW_0:23; then A57: b "\/" y1 = y1 by YELLOW_5:8; x"\/"(z"/\"y) <= (x"\/"z)"/\"(x"\/"y) by Th7; then (x"\/"(z"/\"y))"/\"(z"\/"(x"/\"y)) <= ((x"\/"z)"/\"(x"\/"y))"/\"(( z "\/" x)"/\"(z"\/"y)) by A26,YELLOW_3:2; then (x"\/"b)"/\"(z"\/"b) <= ((x"\/"y)"/\"(x"\/"z))"/\"(x"\/"z)"/\"(z"\/"y ) by A47,A39,LATTICE3:16; then (x"\/"b)"/\"(z"\/"b) <= (x"\/"y)"/\"((x"\/"z)"/\"(x"\/"z))"/\"(z "\/" y) by LATTICE3:16; then (x"\/"b)"/\"(z"\/"b) <= (x"\/"y)"/\"(x"\/"z)"/\"(z"\/"y) by YELLOW_5:2 ; then A58: (x"\/"b)"/\"(z"\/"b) <= t by LATTICE3:16; x1 <= t by YELLOW_0:23; then A59: t "/\" x1 = x1 by YELLOW_5:10; A60: z1 "/\" y1 = (z"\/"b)"/\"(t "/\" ((y"\/"b)"/\"t)) by LATTICE3:16 .= (z"\/"b)"/\"(t "/\" t "/\" (y"\/"b)) by LATTICE3:16 .= (z"\/"b)"/\"((y"\/"b) "/\" t) by YELLOW_5:2 .= (z"\/"b)"/\"(y"\/"b) "/\" t by LATTICE3:16 .= (z "\/"(y"/\"x))"/\"(y "\/"(z"/\"x)) by A30,A39,A48,YELLOW_5:10 .= (y"/\"(z "\/"(y"/\"x))) "\/"(z"/\"x) by A1,A43 .= b by A1,A55; (z"/\"y)"\/"(z"/\"x) <= z"/\"(y"\/"x) by Th6; then ((z"/\"y)"\/"(z"/\"x))"\/"((z"/\"y)"\/"(y"/\"x)) <= (z"/\"(y"\/"x) ) "\/" (y"/\"(z"\/"x)) by A54,YELLOW_3:3; then (z"/\"x)"\/"((z"/\"y)"\/"((z"/\"y)"\/"(y"/\"x))) <= (z"/\"(y"\/"x) ) "\/" (y"/\"(z"\/"x)) by LATTICE3:14; then (z"/\"x)"\/"(((z"/\"y)"\/"(z"/\"y))"\/"(y"/\"x)) <= (z"/\"(y"\/"x) ) "\/" (y"/\"(z"\/"x)) by LATTICE3:14; then (z"/\"y)"\/"(z"/\"y)"\/"(z"/\"x)"\/"(y"/\"x) <= (z"/\"(y"\/"x)) "\/" (y "/\"(z"\/"x)) by LATTICE3:14; then (z"/\"y)"\/"(z"/\"x)"\/"(y"/\"x) <= (z"/\"(y"\/"x)) "\/" (y"/\"(z "\/" x)) by YELLOW_5:1; then A61: b <= (z"/\"t)"\/"(y"/\"t) by A22,A52,LATTICE3:14; A62: (x"/\"z)"\/"(z"/\"y) <= z "/\" ( x "\/"y) by Th6; A63: z"/\"y <= z by YELLOW_0:23; (x"/\"z)"\/"(x"/\"y) <= x"/\"(z"\/"y) by Th6; then ((x"/\"z)"\/"(x"/\"y))"\/"((x"/\"z)"\/"(z"/\"y)) <= (x"/\"(z"\/"y) ) "\/" (z"/\"(x"\/"y)) by A62,YELLOW_3:3; then (x"/\"y)"\/"((x"/\"z)"\/"((x"/\"z)"\/"(z"/\"y))) <= (x"/\"(z"\/"y) ) "\/" (z"/\"(x"\/"y)) by LATTICE3:14; then (x"/\"y)"\/"(((x"/\"z)"\/"(x"/\"z))"\/"(z"/\"y)) <= (x"/\"(z"\/"y) ) "\/" (z"/\"(x"\/"y)) by LATTICE3:14; then (x"/\"z)"\/"(x"/\"z)"\/"(x"/\"y)"\/"(z"/\"y) <= (x"/\"(z"\/"y)) "\/" (z "/\"(x"\/"y)) by LATTICE3:14; then (x"/\"z)"\/"(x"/\"y)"\/"(z"/\"y) <= (x"/\"(z"\/"y)) "\/" (z"/\"(x "\/" y)) by YELLOW_5:1; then A64: b <= (x"/\"t)"\/"(z"/\"t) by A18,A52,LATTICE3:14; (x"/\"y) <= (z"\/" x) by YELLOW_5:5; then (x"/\"y) "/\" (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/" x) by A51 ,YELLOW_3:2; then (x"/\"y) <= t by YELLOW_5:2; then (x"/\"y)"\/"(y"/\"z) <= t"\/"t by A17,YELLOW_3:3; then (x"/\"y)"\/"(y"/\"z) <= t by YELLOW_5:1; then (x"/\"y)"\/"(y"/\"z)"\/"(z"/\"x) <= t"\/"t by A21,YELLOW_3:3; then A65: b <= t by YELLOW_5:1; then z1 = (z"/\"t)"\/"b by A1; then A66: x1 "\/" z1 = ((x"/\"t)"\/"b) "\/" ((z"/\"t)"\/"b) by A1,A65 .= (x"/\"t)"\/"(b "\/" ((z"/\"t)"\/"b)) by LATTICE3:14 .= (x"/\"t)"\/"(b "\/" b "\/" (z"/\"t)) by LATTICE3:14 .= (x"/\"t)"\/"((z"/\"t) "\/" b) by YELLOW_5:1 .= (x"/\"t)"\/"(z"/\"t) "\/" b by LATTICE3:14 .= (x "/\"(z"\/"y))"\/"(z "/\"(x"\/"y)) by A18,A52,A64,YELLOW_5:8 .= (z"\/"(x "/\"(z"\/"y))) "/\"(x"\/"y) by A1,A29 .= (z"\/"x)"/\"(z"\/"y)"/\"(x"\/"y) by A1,A33 .= t by LATTICE3:16; A67: y1 = (y"/\"t)"\/"b by A1,A65; then A68: x1 "\/" y1 = ((x"/\"t)"\/"b) "\/" ((y"/\"t)"\/"b) by A1,A65 .= (x"/\"t)"\/"(b "\/" ((y"/\"t)"\/"b)) by LATTICE3:14 .= (x"/\"t)"\/"(b "\/" b "\/" (y"/\"t)) by LATTICE3:14 .= (x"/\"t)"\/"((y"/\"t) "\/" b) by YELLOW_5:1 .= (x"/\"t)"\/"(y"/\"t) "\/" b by LATTICE3:14 .= (x "/\"(y"\/"z))"\/"(y "/\"(x"\/"z)) by A18,A22,A40,YELLOW_5:8 .= (y"\/"(x "/\"(y"\/"z))) "/\"(x"\/"z) by A1,A46 .= t by A1,A25; A69: z1 "\/" y1 = ((z"/\"t)"\/"b) "\/" ((y"/\"t)"\/"b) by A1,A65,A67 .= (z"/\"t)"\/"(b "\/" ((y"/\"t)"\/"b)) by LATTICE3:14 .= (z"/\"t)"\/"(b "\/" b "\/" (y"/\"t)) by LATTICE3:14 .= (z"/\"t)"\/"((y"/\"t) "\/" b) by YELLOW_5:1 .= (z"/\"t)"\/"(y"/\"t) "\/" b by LATTICE3:14 .= (z "/\"(y"\/"x))"\/"(y "/\"(z"\/"x)) by A22,A52,A61,YELLOW_5:8 .= (y"\/"(z "/\"(y"\/"x))) "/\"(z"\/"x) by A1,A38 .= t by A1,A44; A70: x1 "/\" z1 = (x"\/"b)"/\"(t "/\" ((z"\/"b)"/\"t)) by LATTICE3:16 .= (x"\/"b)"/\"(t "/\" t "/\" (z"\/"b)) by LATTICE3:16 .= (x"\/"b)"/\"((z"\/"b) "/\" t) by YELLOW_5:2 .= (x"\/"b)"/\"(z"\/"b) "/\" t by LATTICE3:16 .= (x "\/"(z"/\"y))"/\"(z "\/"(x"/\"y)) by A47,A39,A58,YELLOW_5:10 .= (z"/\"(x "\/"(z"/\"y))) "\/"(x"/\"y) by A1,A32 .= (z"/\"x)"\/"(z"/\"y)"\/"(x"/\"y) by A1,A63 .= b by LATTICE3:14; then b <= z1 by YELLOW_0:23; then A71: b "\/" z1 = z1 by YELLOW_5:8; b <= x1 by A56,YELLOW_0:23; then A72: b "\/" x1 = x1 by YELLOW_5:8; thus ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c"/\"e = c & d"/\" e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e & b"\/"d = e & c"\/" d = e proof take b,x1,y1,z1,t; thus b<>x1 by A14,A68,A66,A60,A57,A71,YELLOW_5:2; thus b<>y1 by A14,A68,A70,A69,A72,A71,YELLOW_5:2; thus b<>z1 by A14,A56,A66,A69,A72,A57,YELLOW_5:2; thus b<>t by A14; now assume A73: x1=y1; then x1"/\"y1=x1 by YELLOW_5:2; hence contradiction by A14,A68,A56,A73,YELLOW_5:1; end; hence x1<>y1; now assume A74: x1=z1; then x1"/\"z1=x1 by YELLOW_5:2; hence contradiction by A14,A66,A70,A74,YELLOW_5:1; end; hence x1<>z1; thus x1<>t by A14,A56,A70,A69,A49,A41,YELLOW_5:1; now assume A75: y1=z1; then y1"/\"z1=y1 by YELLOW_5:2; hence contradiction by A14,A69,A60,A75,YELLOW_5:1; end; hence y1<>z1; thus y1<>t by A14,A56,A66,A60,A59,A41,YELLOW_5:1; thus z1<>t by A14,A68,A70,A60,A59,A49,YELLOW_5:1; b <= x1 by A56,YELLOW_0:23; hence b"/\"x1 = b by YELLOW_5:10; b <= y1 by A56,YELLOW_0:23; hence b"/\"y1 = b by YELLOW_5:10; b <= z1 by A70,YELLOW_0:23; hence b"/\"z1 = b by YELLOW_5:10; x1 <= t by A68,YELLOW_0:22; hence x1"/\"t = x1 by YELLOW_5:10; y1 <= t by A68,YELLOW_0:22; hence y1"/\"t = y1 by YELLOW_5:10; z1 <= t by A66,YELLOW_0:22; hence z1"/\"t = z1 by YELLOW_5:10; thus x1"/\"y1 = b by A56; thus x1"/\"z1 = b by A70; thus y1"/\"z1 = b by A60; thus x1"\/"y1 = t by A68; thus x1"\/"z1 = t by A66; thus thesis by A69; end; end; hence thesis; end; theorem for L being LATTICE st L is modular holds L is distributive iff not ex K being full Sublattice of L st M_3,K are_isomorphic proof let L be LATTICE; assume A1: L is modular; thus L is distributive implies not ex K being full Sublattice of L st M_3,K are_isomorphic proof assume L is distributive; then not ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c"/\"e = c & d"/\" e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e & b"\/"d = e & c"\/" d = e) by Lm3; hence thesis by Th10; end; assume not ex K being full Sublattice of L st M_3,K are_isomorphic; then not ex a,b,c,d,e being Element of L st (a,b,c,d,e are_mutually_distinct & a"/\"b = a & a"/\"c = a & a"/\"d = a & b "/\"e = b & c"/\"e = c & d"/\" e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b "\/"c = e & b"\/"d = e & c"\/" d = e) by Th10; hence thesis by A1,Lm3; end; begin:: Intervals of a lattice definition let L be non empty RelStr; let a,b be Element of L; func [#a,b#] -> Subset of L means :Def4: for c being Element of L holds c in it iff a <= c & c <= b; existence proof defpred P[object] means ex c1 being Element of L st c1=$1 & a <= c1 & c1 <= b; consider S being set such that A1: for c being object holds c in S iff c in the carrier of L & P[c] from XBOOLE_0:sch 1; for c being object holds c in S implies c in the carrier of L by A1; then reconsider S as Subset of L by TARSKI:def 3; reconsider S as Subset of L; take S; thus for c being Element of L holds c in S iff a <= c & c <= b proof let c be Element of L; thus c in S implies a <= c & c <= b proof assume c in S; then ex c1 being Element of L st c1=c & a <= c1 & c1 <= b by A1; hence thesis; end; thus thesis by A1; end; end; uniqueness proof let x,y be Subset of L; assume that A2: for c being Element of L holds c in x iff a <= c & c <= b and A3: for c being Element of L holds c in y iff a <= c & c <= b; now let c1 be object; assume A4: c1 in y; then reconsider c = c1 as Element of L; c in y iff a <= c & c <= b by A3; hence c1 in x by A2,A4; end; then A5: y c= x; now let c1 be object; assume A6: c1 in x; then reconsider c = c1 as Element of L; c in x iff a <= c & c <= b by A2; hence c1 in y by A3,A6; end; then x c= y; hence thesis by A5; end; end; definition let L be non empty RelStr; let IT be Subset of L; attr IT is interval means ex a,b being Element of L st IT = [#a,b#]; end; registration let L be non empty reflexive transitive RelStr; cluster non empty interval -> directed for (Subset of L); coherence proof let M be Subset of L; assume A1: M is non empty interval; then consider z being object such that A2: z in M; reconsider z as Element of L by A2; consider a,b being Element of L such that A3: M = [#a,b#] by A1; A4: z <= b by A3,A2,Def4; a <= z by A3,A2,Def4; then A5: a <= b by A4,ORDERS_2:3; let x,y be Element of L; assume that A6: x in M and A7: y in M; take b; b <= b; hence b in M by A3,A5,Def4; thus x <= b & y <= b by A3,A6,A7,Def4; end; cluster non empty interval -> filtered for (Subset of L); coherence proof let M be Subset of L; assume A8: M is non empty interval; then consider z being object such that A9: z in M; reconsider z as Element of L by A9; consider a,b being Element of L such that A10: M = [#a,b#] by A8; A11: z <= b by A10,A9,Def4; a <= z by A10,A9,Def4; then A12: a <= b by A11,ORDERS_2:3; let x,y be Element of L; assume that A13: x in M and A14: y in M; take a; a <= a; hence a in M by A10,A12,Def4; thus a <= x & a <= y by A10,A13,A14,Def4; end; end; registration let L be non empty RelStr; let a,b be Element of L; cluster [#a,b#] -> interval; coherence; end; theorem for L being non empty reflexive transitive RelStr, a,b being Element of L holds [#a,b#] = uparrow a /\ downarrow b proof let L be non empty reflexive transitive RelStr; let a,b be Element of L; thus [#a,b#] c= uparrow a /\ downarrow b proof let x be object; A1: a in {a} by TARSKI:def 1; A2: b in {b} by TARSKI:def 1; assume A3: x in [#a,b#]; then reconsider y=x as Element of L; y <= b by A3,Def4; then y in {z where z is Element of L : ex w being Element of L st z <= w & w in {b}} by A2; then A4: y in downarrow {b} by WAYBEL_0:14; a <= y by A3,Def4; then y in {z where z is Element of L : ex w being Element of L st z >= w & w in {a}} by A1; then y in uparrow {a} by WAYBEL_0:15; hence thesis by A4,XBOOLE_0:def 4; end; thus uparrow a /\ downarrow b c= [#a,b#] proof let x be object; assume A5: x in uparrow a /\ downarrow b; then x in uparrow {a} by XBOOLE_0:def 4; then x in {z where z is Element of L : ex w being Element of L st z >= w & w in {a}} by WAYBEL_0:15; then consider y1 being Element of L such that A6: x=y1 and A7: ex w being Element of L st y1 >= w & w in {a}; A8: a <= y1 by A7,TARSKI:def 1; x in downarrow {b} by A5,XBOOLE_0:def 4; then x in {z where z is Element of L : ex w being Element of L st z <= w & w in {b}} by WAYBEL_0:14; then ex y2 being Element of L st x=y2 & ex w being Element of L st y2 <= w & w in {b}; then y1 <= b by A6,TARSKI:def 1; hence thesis by A6,A8,Def4; end; end; registration let L be with_infima Poset; let a,b be Element of L; cluster subrelstr[#a,b#] -> meet-inheriting; coherence proof let x,y be Element of L; set ab = subrelstr[#a,b#]; assume that A1: x in the carrier of ab and A2: y in the carrier of ab and ex_inf_of {x,y},L; A3: x in [#a,b#] by A1,YELLOW_0:def 15; then A4: x <= b by Def4; A5: inf {x,y} = x"/\"y by YELLOW_0:40; then inf {x,y} <= x by YELLOW_0:23; then A6: inf {x,y} <= b by A4,YELLOW_0:def 2; y in [#a,b#] by A2,YELLOW_0:def 15; then A7: a <= y by Def4; a <= x by A3,Def4; then a <= inf {x,y} by A7,A5,YELLOW_0:23; then inf {x,y} in [#a,b#] by A6,Def4; hence thesis by YELLOW_0:def 15; end; end; registration let L be with_suprema Poset; let a,b be Element of L; cluster subrelstr[#a,b#] -> join-inheriting; coherence proof let x,y be Element of L; set ab = subrelstr([#a,b#]); assume that A1: x in the carrier of ab and A2: y in the carrier of ab and ex_sup_of {x,y},L; A3: x in [#a,b#] by A1,YELLOW_0:def 15; then A4: a <= x by Def4; A5: sup {x,y} = x"\/"y by YELLOW_0:41; then x <= sup {x,y} by YELLOW_0:22; then A6: a <= sup {x,y} by A4,YELLOW_0:def 2; y in [#a,b#] by A2,YELLOW_0:def 15; then A7: y <= b by Def4; x <= b by A3,Def4; then sup {x,y} <= b by A7,A5,YELLOW_0:22; then sup {x,y} in [#a,b#] by A6,Def4; hence thesis by YELLOW_0:def 15; end; end; theorem for L being LATTICE, a,b being Element of L holds L is modular implies subrelstr[#b,a"\/"b#],subrelstr[#a"/\" b,a#] are_isomorphic proof let L be LATTICE; let a,b be Element of L; assume A1: L is modular; defpred P[object,object] means ($2 is Element of L & (for X being Element of L,Y being Element of L holds ($1=X & $2=Y) implies Y = X "/\" a)); A2: for x being object st x in the carrier of subrelstr[#b,a"\/"b#] ex y being object st y in the carrier of subrelstr[#a"/\"b,a#] & P[x,y] proof let x be object; assume x in the carrier of subrelstr[#b,a"\/"b#]; then A3: x in [#b,a"\/"b#] by YELLOW_0:def 15; then reconsider x1 = x as Element of L; take y = a "/\" x1; x1 <= a"\/"b by A3,Def4; then y <= a"/\"(a"\/"b) by YELLOW_5:6; then A4: y <= a by LATTICE3:18; b <= x1 by A3,Def4; then a"/\"b <= y by YELLOW_5:6; then y in [#(a"/\"b),a#] by A4,Def4; hence y in the carrier of subrelstr([#(a"/\"b),a#]) by YELLOW_0:def 15; thus thesis; end; consider f being Function of the carrier of subrelstr[#b,a"\/"b#],the carrier of subrelstr[#(a"/\"b),a#] such that A5: for x being object st x in the carrier of subrelstr[#b,a"\/"b#] holds P[x,f.x] from FUNCT_2:sch 1(A2); reconsider f as Function of subrelstr[#b,a"\/"b#],subrelstr[#(a"/\"b),a#]; take f; thus f is isomorphic proof A6: b <= a"\/"b by YELLOW_0:22; b <= b; then b in [#b,a"\/"b#] by A6,Def4; then reconsider s1 = subrelstr([#b,b"\/" a#]) as non empty full Sublattice of L by YELLOW_0:def 15; A7: a"/\"b <= a by YELLOW_0:23; a"/\"b <= a"/\"b; then a"/\"b in [#a"/\"b,a#] by A7,Def4; then reconsider s2 = subrelstr[#(a"/\" b),a#] as non empty full Sublattice of L by YELLOW_0:def 15; reconsider f1 = f as Function of s1,s2; dom f1 = the carrier of subrelstr[#b,a"\/"b#] by FUNCT_2:def 1; then A8: dom f1 = [#b,a"\/"b#] by YELLOW_0:def 15; the carrier of subrelstr[#(a"/\"b),a#] c= rng f1 proof let y be object; assume y in the carrier of subrelstr[#(a"/\"b),a#]; then A9: y in [#(a"/\"b),a#] by YELLOW_0:def 15; then reconsider Y = y as Element of L; A10: a"/\"b <= Y by A9,Def4; then (a"/\"b)"\/"b <= Y"\/"b by WAYBEL_1:2; then A11: b <= Y"\/"b by LATTICE3:17; A12: Y <= a by A9,Def4; then Y"\/"b <= a"\/"b by WAYBEL_1:2; then A13: Y"\/"b in [#b,a"\/"b#] by A11,Def4; then A14: Y"\/"b in the carrier of subrelstr([#b,a"\/"b#]) by YELLOW_0:def 15; then reconsider f1yb = f1.(Y"\/"b) as Element of L by A5; f1yb = (Y"\/"b)"/\"a by A5,A14 .= Y"\/"(b"/\"a) by A1,A12 .= Y by A10,YELLOW_5:8; hence thesis by A8,A13,FUNCT_1:def 3; end; then A15: rng f1 = the carrier of subrelstr[#(a"/\"b),a#]; A16: for x,y being Element of s1 holds x <= y iff f1.x <= f1.y proof let x,y be Element of s1; A17: the carrier of s1 = [#b,a"\/"b#] by YELLOW_0:def 15; then x in [#b,a"\/"b#]; then reconsider X = x as Element of L; y in [#b,a"\/"b#] by A17; then reconsider Y = y as Element of L; reconsider f1Y = f1.Y as Element of L by A5; reconsider f1X = f1.X as Element of L by A5; thus x <= y implies f1.x <= f1.y proof assume x <= y; then A18: [x,y] in the InternalRel of s1 by ORDERS_2:def 5; the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13; then A19: X <= Y by A18,ORDERS_2:def 5; A20: f1Y = Y"/\"a by A5; f1X = X"/\"a by A5; then f1X <= f1Y by A19,A20,WAYBEL_1:1; hence thesis by YELLOW_0:60; end; thus f1.x <= f1.y implies x <= y proof assume f1.x <= f1.y; then A21: [f1.x,f1.y] in the InternalRel of s2 by ORDERS_2:def 5; the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13; then A22: f1X <= f1Y by A21,ORDERS_2:def 5; A23: f1Y = Y"/\"a by A5; A24: b <= X by A17,Def4; f1X = X"/\"a by A5; then b"\/"(a"/\"X) <= b"\/"(a"/\"Y) by A22,A23,WAYBEL_1:2; then A25: (b"\/"a)"/\"X <= b"\/"(a"/\"Y) by A1,A24; A26: X <= b"\/"a by A17,Def4; b <= Y by A17,Def4; then (b"\/"a)"/\"X <= (b"\/"a)"/\"Y by A1,A25; then A27: X <= (b"\/"a)"/\"Y by A26,YELLOW_5:10; Y <= b"\/"a by A17,Def4; then X <= Y by A27,YELLOW_5:10; hence thesis by YELLOW_0:60; end; end; f1 is one-to-one proof let x1,x2 be object; assume that A28: x1 in dom f1 and A29: x2 in dom f1 and A30: f1.x1 = f1.x2; reconsider X2 = x2 as Element of L by A8,A29; A31: b <= X2 by A8,A29,Def4; reconsider X1 = x1 as Element of L by A8,A28; A32: b <= X1 by A8,A28,Def4; reconsider f1X1 = f1.X1 as Element of L by A5,A28; A33: f1X1 = X1 "/\" a by A5,A28; reconsider f1X2 = f1.X2 as Element of L by A5,A29; A34: f1X2 = X2 "/\" a by A5,A29; A35: X2 <= a"\/"b by A8,A29,Def4; X1 <= a"\/"b by A8,A28,Def4; then X1 = (b "\/" a) "/\" X1 by YELLOW_5:10 .= b "\/" (a "/\" X2) by A1,A30,A32,A33,A34 .= (b "\/" a) "/\" X2 by A1,A31 .= X2 by A35,YELLOW_5:10; hence thesis; end; hence thesis by A15,A16,WAYBEL_0:66; end; end; registration cluster finite non empty for LATTICE; existence proof set D = {{}}; set R = the Order of D; reconsider A = RelStr (#D,R#) as with_infima with_suprema Poset; take A; thus thesis; end; end; registration cluster finite -> lower-bounded for Semilattice; coherence proof let L be Semilattice; defpred P[set] means ex x being Element of L st x is_<=_than $1; A1: P[{}] proof set a = the Element of L; take a; let b be Element of L; assume b in {}; hence thesis; end; A2: for x,B being set st x in the carrier of L & B c= the carrier of L & P [B] holds P[B \/ {x}] proof let x,B be set; assume that A3: x in the carrier of L and B c= the carrier of L; reconsider y=x as Element of L by A3; given a being Element of L such that A4: a is_<=_than B; take b = a"/\"y; let c be Element of L; A5: now assume c in B; then A6: a <= c by A4; a"/\"y <= a by YELLOW_0:23; hence a"/\"y <= c by A6,ORDERS_2:3; end; A7: now assume c in {x}; then c = y by TARSKI:def 1; hence b <= c by YELLOW_0:23; end; assume c in B \/ {x}; hence thesis by A5,A7,XBOOLE_0:def 3; end; assume L is finite; then A8: the carrier of L is finite; thus P[the carrier of L] from FINSET_1:sch 2(A8,A1,A2); end; end; registration cluster finite -> complete for LATTICE; coherence proof let L be LATTICE; assume A1: L is finite; for x being Subset of L holds ex_sup_of x,L proof let x be Subset of L; per cases; suppose x = {}; hence thesis by A1,YELLOW_0:42; end; suppose A2: x <> {}; x is finite by A1,FINSET_1:1; hence thesis by A2,YELLOW_0:54; end; end; hence thesis by YELLOW_0:53; end; end;