:: On the Characterization of Modular and Distributive Lattices
:: by Adam Naumowicz
::
:: Received April 3, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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;
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,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;
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 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;