Copyright (c) 1998 Association of Mizar Users
environ
vocabulary ORDINAL1, BOOLE, RELAT_2, LATTICE3, ORDERS_1, LATTICES, WAYBEL_0,
YELLOW_1, CAT_1, FILTER_2, WELLORD1, PRE_TOPC, YELLOW_0, FUNCT_1, SEQM_3,
RELAT_1, ORDINAL2, MEASURE5, QUANTAL1, FINSET_1, BHSP_3, YELLOW11;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
PRE_TOPC, STRUCT_0, ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1,
YELLOW_2, WAYBEL_1, LATTICE5, FINSET_1, GROUP_1, WAYBEL_0, ORDINAL1;
constructors LATTICE3, GROUP_1, ORDERS_3, WAYBEL_1, ENUMSET1;
clusters STRUCT_0, LATTICE3, YELLOW_0, ORDERS_1, FINSET_1, YELLOW_1, RELSET_1,
XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE;
definitions TARSKI, YELLOW_0, WAYBEL_1, FUNCT_1, WAYBEL_0, LATTICE3, XBOOLE_0;
theorems WAYBEL_1, YELLOW_0, YELLOW_3, YELLOW_5, LATTICE3, STRUCT_0, TARSKI,
FUNCT_2, WAYBEL_0, ZFMISC_1, FUNCT_1, ORDERS_1, YELLOW_1, ENUMSET1,
CARD_1, GROUP_1, FINSET_1, CARD_5, ORDINAL1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, FINSET_1, XBOOLE_0;
begin
reserve x for set;
:: Preliminaries
theorem Th1:
3 = {0,1,2}
proof
thus 3 = succ 2
.= {0,1} \/ {2} by CARD_5:1,ORDINAL1:def 1
.= {0,1,2} by ENUMSET1:43;
end;
theorem Th2:
2\1={1}
proof
thus 2\1 c= {1}
proof
let x be set;
assume x in 2\1;
then x in {0,1} & not x in {0} by CARD_5:1,XBOOLE_0:def 4;
then (x=0 or x=1) & x <> 0 by TARSKI:def 1,def 2;
hence thesis by TARSKI:def 1;
end;
let x be set;
assume x in {1};
then x = 1 by TARSKI:def 1;
then x in {0,1} & not x in {0} by TARSKI:def 1,def 2;
hence thesis by CARD_5:1,XBOOLE_0:def 4;
end;
theorem Th3:
3\1 = {1,2}
proof
thus 3\1 c= {1,2}
proof
let x;
assume x in 3\1;
then x in {0,1,2} & not x in {0} by Th1,CARD_5:1,XBOOLE_0:def 4;
then (x=0 or x=1 or x=2) & x <> 0 by ENUMSET1:13,TARSKI:def 1;
hence x in {1,2} by TARSKI:def 2;
end;
thus {1,2} c= 3\1
proof
let x;
assume x in {1,2};
then x=1 or x=2 by TARSKI:def 2;
then x in {0,1,2} & not x in {0} by ENUMSET1:14,TARSKI:def 1;
hence x in 3\1 by Th1,CARD_5:1,XBOOLE_0:def 4;
end;
end;
theorem Th4:
3\2 = {2}
proof
thus 3\2 c= {2}
proof
let x;
assume x in 3\2;
then x in {0,1,2} & not x in {0,1} by Th1,CARD_5:1,XBOOLE_0:def 4;
then (x=0 or x=1 or x=2) & (x <> 0 & x <> 1)
by ENUMSET1:13,TARSKI:def 2;
hence x in {2} by TARSKI:def 1;
end;
thus {2} c= 3\2
proof
let x;
assume x in {2};
then x=2 by TARSKI:def 1;
then x in {0,1,2} & not x in {0,1} by ENUMSET1:14,TARSKI:def 2;
hence x in 3\2 by Th1,CARD_5:1,XBOOLE_0:def 4;
end;
end;
Lm1:
3\2 c= 3\1
proof
let x be set;
assume x in 3\2;
then x=2 by Th4,TARSKI:def 1;
hence x in 3\1 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 a"\/"b = a by YELLOW_0:24;
end;
assume a"\/"b = a;
then b <= a by YELLOW_0:22;
hence a"/\"b = b 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;
b <= b"\/"c & c <= b"\/"c & a <= a by YELLOW_0:22;
then a"/\"b <= a"/\"(b"\/"c) & a"/\"c <= a"/\"(b"\/"c) by YELLOW_3:2;
hence thesis by 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;
b"/\"c <= b & b"/\"c <= c & a <= a by YELLOW_0:23;
then a"\/"(b"/\"c) <= a"\/"b & a"\/"(b"/\"c) <= a"\/"c by YELLOW_3:3;
hence thesis by 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;
assume
A1: a <= c;
A2: b"/\"c <= c & b"/\"c <= b & a <= a by YELLOW_0:23;
then A3: a"\/"(b"/\"c) <= c by A1,YELLOW_0:22;
a"\/"(b"/\"c) <= a"\/"b by A2,YELLOW_3:3;
hence thesis by A3,YELLOW_0:23;
end;
definition
func N_5 -> RelStr equals :Def1:
InclPoset {0, 3 \ 1, 2, 3 \ 2, 3};
correctness;
end;
definition
cluster N_5 -> strict reflexive transitive antisymmetric;
correctness by Def1;
cluster N_5 -> with_infima with_suprema;
correctness
proof
set Z = {0, 3 \ 1, 2, 3 \ 2, 3};
set N = InclPoset Z;
A1: Z <> {} by ENUMSET1:24;
A2: N is with_suprema
proof
now
let x,y be set;
assume x in Z & y in Z;
then A3: (x=0 or x=3\1 or x=2 or x=3\2 or x=3) &
(y=0 or y=3\1 or y=2 or y=3\2 or y=3) by ENUMSET1:23;
A4: (3\1) \/ 2 = {0,1,1,2} by Th3,CARD_5:1,ENUMSET1:45
.= {1,1,0,2} by ENUMSET1:110
.= {1,0,2} by ENUMSET1:71
.= {0,1,2} by ENUMSET1:99;
A5: (3\1) \/ (3\2) = {1,2} by Th3,Th4,ZFMISC_1:14;
3\1 c= 3 by XBOOLE_1:36;
then A6: (3\1) \/ 3 = 3 by XBOOLE_1:12;
A7: 2 \/ (3\2) = 2 \/ 3 & 2 c= 3 by CARD_1:56,XBOOLE_1:39;
then A8: 2 \/ 3 = 3 by XBOOLE_1:12;
3\2 c= 3 by XBOOLE_1:36;
then (3\2) \/ 3 = 3 by XBOOLE_1:12;
hence x \/ y in Z by A3,A4,A5,A6,A7,A8,Th1,Th3,ENUMSET1:24;
end;
hence thesis by A1,YELLOW_1:11;
end;
N is with_infima
proof
let x,y be Element of N;
A9: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st z <= x & z <= y &
for z' being Element of N st z' <= x & z' <= y holds z' <= z
proof
per cases by A1,A9,ENUMSET1:23;
suppose
x = 0 & y = 0;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
x = 0 & y = 3\1;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 0 & y = 2;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 0 & y = 3\2;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 0 & y = 3;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 3\1 & y = 0;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
x = 3\1 & y = 3\1;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A10: x = 3\1 & y = 2;
0 in Z by ENUMSET1:24;
then 0 in the carrier of N by YELLOW_1:1;
then reconsider z = 0 as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:2;
hence z <= x & z <= y by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A11: z'=0 or z'=3\1 or z'=2 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume z' <= x & z' <= y;
then A12: z' c= 3\1 & z' c= 2 by A1,A10,YELLOW_1:3;
A13: now
assume z'= 3\1;
then 2 in z' & not 2 in 2 by Th3,TARSKI:def 2;
hence contradiction by A12;
end;
A14: now
assume
z'= 2;
then 0 in z' & not 0 in 3\1 by Th3,CARD_5:1,TARSKI:def 2;
hence contradiction by A12;
end;
A15: now
assume z'= 3\2;
then 2 in z' & not 2 in 2 by Th4,TARSKI:def 1;
hence contradiction by A12;
end;
now
assume z'= 3;
then 2 in z' & not 2 in 2 by Th1,ENUMSET1:14;
hence contradiction by A12;
end;
hence z' <= z by A1,A11,A13,A14,A15,YELLOW_1:3;
suppose
A16: x = 3\1 & y = 3\2;
(3\1) /\ (3\2) = {2} by Th3,Th4,ZFMISC_1:19;
then x /\ y in Z by A16,Th4,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A17: x = 3\1 & y = 3;
(3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3\1;
then x /\ y in Z by A17,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 2 & y = 0;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A18: x = 2 & y = 3\1;
0 in Z by ENUMSET1:24;
then 0 in the carrier of N by YELLOW_1:1;
then reconsider z = 0 as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:2;
hence z <= x & z <= y by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A19: z'=0 or z'=3\1 or z'=2 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume z' <= x & z' <= y;
then A20: z' c= 3\1 & z' c= 2 by A1,A18,YELLOW_1:3;
A21: now
assume z'= 3\1;
then 2 in z' & not 2 in 2 by Th3,TARSKI:def 2;
hence contradiction by A20;
end;
A22: now
assume
z'= 2;
then 0 in z' & not 0 in 3\1 by Th3,CARD_5:1,TARSKI:def 2;
hence contradiction by A20;
end;
A23: now
assume z'= 3\2;
then 2 in z' & not 2 in 2 by Th4,TARSKI:def 1;
hence contradiction by A20;
end;
now
assume z'= 3;
then 2 in z' & not 2 in 2 by Th1,ENUMSET1:14;
hence contradiction by A20;
end;
hence z' <= z by A1,A19,A21,A22,A23,YELLOW_1:3;
suppose
x = 2 & y = 2;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A24: x = 2 & y = 3\2;
2 misses (3\2) by XBOOLE_1:79;
then 2 /\ (3\2) = 0 by XBOOLE_0:def 7;
then x /\ y in Z by A24,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A25: x = 2 & y = 3;
2 c= 3 by CARD_1:56;
then 2 /\ 3 = 2 by XBOOLE_1:28;
then x /\ y in Z by A25,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 3\2 & y = 0;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A26: x = 3\2 & y = 3\1;
(3\1) /\ (3\2) = {2} by Th3,Th4,ZFMISC_1:19;
then x /\ y in Z by A26,Th4,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A27: x = 3\2 & y = 2;
2 misses (3\2) by XBOOLE_1:79;
then 2 /\ (3\2) = 0 by XBOOLE_0:def 7;
then x /\ y in Z by A27,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
x = 3\2 & y = 3\2;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A28: x = 3\2 & y = 3;
(3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49
.= 3\2;
then x /\ y in Z by A28,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose x = 3 & y = 0;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A29: x = 3 & y = 3\1;
(3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3\1;
then x /\ y in Z by A29,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A30: x = 3 & y = 2;
2 c= 3 by CARD_1:56;
then 2 /\ 3 = 2 by XBOOLE_1:28;
then x /\ y in Z by A30,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
A31: x = 3 & y = 3\2;
(3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49
.= 3\2;
then x /\ y in Z by A31,ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
suppose
x = 3 & y = 3;
then x /\ y in Z by ENUMSET1:24;
then x /\ y in the carrier of N by YELLOW_1:1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by A1,YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by A1,YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by A1,YELLOW_1:3;
end;
end;
hence thesis by A2,Def1;
end;
end;
definition
func M_3 -> RelStr equals :Def2:
InclPoset{ 0, 1, 2 \ 1, 3 \ 2, 3 };
correctness;
end;
definition
cluster M_3 -> strict reflexive transitive antisymmetric;
correctness by Def2;
cluster M_3 -> with_infima with_suprema;
correctness
proof
set Z = { 0, 1, 2 \ 1, 3 \ 2, 3 };
set N = InclPoset Z;
A1: Z <> {} by ENUMSET1:24;
A2: N is with_suprema
proof
let x,y be Element of N;
A3: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st x <= z & y <= z &
for z' being Element of N st x <= z' & y <= z' holds z <= z'
proof
per cases by A1,A3,ENUMSET1:23;
suppose
x=0 & y=0;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=0 & y=1;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=0 & y=2\1;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=0 & y=3\2;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=0 & y=3;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=1 & y=0;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
x=1 & y=1;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A4: x=1 & y=2\1;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z
proof
let X be set;
assume X in x; then X=0 by A4,CARD_5:1,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
let X be set;
assume X in y; then X=1 by A4,Th2,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A5: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A6: 1 c= z' & 2\1 c= z' by A1,A4,YELLOW_1:3;
A7: now
assume A8: z'= 0;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A6,A8;
end;
A9: now
assume A10: z'= 1;
1 in 2\1 by Th2,TARSKI:def 1;
then 1 in z' by A6;
hence contradiction by A10;
end;
A11: now
assume A12: z'= 2\1;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A6,A12,Th2,TARSKI:def 1;
end;
now
assume A13: z'= 3\2;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A6,A13,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A5,A7,A9,A11,YELLOW_1:3;
suppose
A14: x=1 & y=3\2;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z
proof
let X be set;
assume X in x; then X=0 by A14,CARD_5:1,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
thus thesis by A14,XBOOLE_1:36;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A15: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A16: 1 c= z' & 3\2 c= z' by A1,A14,YELLOW_1:3;
A17: now
assume A18: z'= 0;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A16,A18;
end;
A19: now
assume A20: z'= 1;
2 in 3\2 by Th4,TARSKI:def 1;
hence contradiction by A16,A20,CARD_5:1,TARSKI:def 1;
end;
A21: now
assume A22: z'= 2\1;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A16,A22,Th2,TARSKI:def 1;
end;
now
assume A23: z'= 3\2;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A16,A23,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A15,A17,A19,A21,YELLOW_1:3;
suppose
A24: x=1 & y=3;
1 c= 3
proof
let X be set;assume X in 1; then X=0 by CARD_5:1,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then 1 \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A24,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=2\1 & y=0;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A25: x=2\1 & y=1;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z
proof
let X be set;
assume X in x; then X=1 by A25,Th2,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
let X be set;
assume X in y; then X=0 by A25,CARD_5:1,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A26: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A27: 1 c= z' & 2\1 c= z' by A1,A25,YELLOW_1:3;
A28: now
assume A29: z'= 0;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A27,A29;
end;
A30: now
assume A31: z'= 1;
1 in 2\1 by Th2,TARSKI:def 1;
then 1 in z' by A27;
hence contradiction by A31;
end;
A32: now
assume A33: z'= 2\1;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A27,A33,Th2,TARSKI:def 1;
end;
now
assume A34: z'= 3\2;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A27,A34,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A26,A28,A30,A32,YELLOW_1:3;
suppose
x=2\1 & y=2\1;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A35: x=2\1 & y=3\2;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z
proof
let X be set;
assume X in x; then X=1 by A35,Th2,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
let X be set;
assume X in y; then X=2 by A35,Th4,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A36: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A37: 2\1 c= z' & 3\2 c= z' by A1,A35,YELLOW_1:3;
A38: now
assume A39: z'= 0;
1 in 2\1 by Th2,TARSKI:def 1;
hence contradiction by A37,A39;
end;
A40: now
assume A41: z'= 1;
1 in 2\1 by Th2,TARSKI:def 1;
then 1 in z' by A37;
hence contradiction by A41;
end;
A42: now
assume A43: z'= 2\1;
2 in 3\2 by Th4,TARSKI:def 1;
hence contradiction by A37,A43,Th2,TARSKI:def 1;
end;
now
assume A44: z'= 3\2;
1 in 2\1 by Th2,TARSKI:def 1;
hence contradiction by A37,A44,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A36,A38,A40,A42,YELLOW_1:3;
suppose
A45: x=2\1 & y=3;
2\1 c= 3
proof
let X be set;assume X in 2\1; then X=1 by Th2,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then (2\1) \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A45,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=3\2 & y=0;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A46: x=3\2 & y=1;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z by A46,XBOOLE_1:36;
thus y c= z
proof
let X be set;
assume X in y; then X=0 by A46,CARD_5:1,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A47: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A48: 1 c= z' & 3\2 c= z' by A1,A46,YELLOW_1:3;
A49: now
assume A50: z'= 0;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A48,A50;
end;
A51: now
assume A52: z'= 1;
2 in 3\2 by Th4,TARSKI:def 1;
hence contradiction by A48,A52,CARD_5:1,TARSKI:def 1;
end;
A53: now
assume A54: z'= 2\1;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A48,A54,Th2,TARSKI:def 1;
end;
now
assume A55: z'= 3\2;
0 in 1 by CARD_5:1,TARSKI:def 1;
hence contradiction by A48,A55,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A47,A49,A51,A53,YELLOW_1:3;
suppose
A56: x=3\2 & y=2\1;
3 in Z by ENUMSET1:24;
then 3 in the carrier of N by YELLOW_1:1;
then reconsider z = 3 as Element of N;
take z;
x c= z & y c= z
proof
thus x c= z
proof
let X be set;
assume X in x; then X=2 by A56,Th4,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
let X be set;
assume X in y; then X=1 by A56,Th2,TARSKI:def 1;
hence X in z by Th1,ENUMSET1:14;
end;
hence x <= z & y <= z by A1,YELLOW_1:3;
let z' be Element of N;
z' is Element of Z by YELLOW_1:1;
then A57: z'=0 or z'=1 or z'=2\1 or z'=3\2 or z'=3 by A1,ENUMSET1:23;
assume x <= z' & y <= z';
then A58: 2\1 c= z' & 3\2 c= z' by A1,A56,YELLOW_1:3;
A59: now
assume A60: z'= 0;
1 in 2\1 by Th2,TARSKI:def 1;
hence contradiction by A58,A60;
end;
A61: now
assume A62: z'= 1;
1 in 2\1 by Th2,TARSKI:def 1;
then 1 in z' by A58;
hence contradiction by A62;
end;
A63: now
assume A64: z'= 2\1;
2 in 3\2 by Th4,TARSKI:def 1;
hence contradiction by A58,A64,Th2,TARSKI:def 1;
end;
now
assume A65: z'= 3\2;
1 in 2\1 by Th2,TARSKI:def 1;
hence contradiction by A58,A65,Th4,TARSKI:def 1;
end;
hence z <= z' by A1,A57,A59,A61,A63,YELLOW_1:3;
suppose
x=3\2 & y=3\2;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A66: x=3\2 & y=3;
3\2 c= 3
proof
let X be set;assume X in 3\2; then X=2 by Th4,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then 3\2 \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A66,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose x=3 & y=0;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A67: x=3 & y=1;
1 c= 3
proof
let X be set;assume X in 1; then X=0 by CARD_5:1,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then 1 \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A67,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A68: x=3 & y=2\1;
2\1 c= 3
proof
let X be set;assume X in 2\1; then X=1 by Th2,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then (2\1) \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A68,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
A69: x=3 & y=3\2;
3\2 c= 3
proof
let X be set;assume X in 3\2; then X=2 by Th4,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then 3\2 \/ 3 = 3 by XBOOLE_1:12;
then x \/ y in Z by A69,ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
suppose
x=3 & y=3;
then x \/ y in Z by ENUMSET1:24;
then x \/ y in the carrier of N by YELLOW_1:1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by A1,YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by A1,YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by A1,YELLOW_1:3;
end;
end;
N is with_infima
proof
now
let x,y be set;
assume x in Z & y in Z;
then A70: (x=0 or x=1 or x=2\1 or x=3\2 or x=3) &
(y=0 or y=1 or y=2\1 or y=3\2 or y=3) by ENUMSET1:23;
1 misses (2\1) by XBOOLE_1:79;
then A71: 1 /\ (2\1) = 0 by XBOOLE_0:def 7;
A72: 1 /\ (3\2) = 0
proof
now let x be set;
assume x in 1 /\ (3\2);
then x in 1 & x in (3\2) by XBOOLE_0:def 3;
then x=0 & x=2 & 0<>2 by Th4,CARD_5:1,TARSKI:def 1;
hence contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
1 c= 3 by CARD_1:56;
then A73: 1 /\ 3 = 1 by XBOOLE_1:28;
A74: (2\1) /\ (3\2) = 0
proof
now let x be set;
assume x in (2\1) /\ (3\2);
then x in (2\1) & x in (3\2) by XBOOLE_0:def 3;
then x=1 & x=2 & 1<>2 by Th2,Th4,TARSKI:def 1;
hence contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
(2\1) c= 3
proof
let x be set;
assume x in 2\1;
then x = 1 by Th2,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then A75: (2\1) /\ 3 = 2\1 by XBOOLE_1:28;
(3\2) c= 3 by XBOOLE_1:36;
then (3\2) /\ 3 = 3\2 by XBOOLE_1:28;
hence x /\ y in Z by A70,A71,A72,A73,A74,A75,ENUMSET1:24;
end;
hence thesis by A1,YELLOW_1:12;
end;
hence thesis by A2,Def2;
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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;
set cn = the carrier of N_5;
A1: cn = {0, 3 \ 1, 2, 3 \ 2, 3} by Def1,YELLOW_1:1;
then A2: 0 in cn & 3\1 in cn & 2 in cn & 3\2 in cn & 3 in cn by ENUMSET1:24;
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
given K being full Sublattice of L
such that
A3: N_5,K are_isomorphic;
consider f being map of N_5,K such that
A4: f is isomorphic by A3,WAYBEL_1:def 8;
A5: K is non empty by A4,WAYBEL_0:def 38;
reconsider K as non empty SubRelStr of L by A4,WAYBEL_0:def 38;
A6: f is one-to-one monotone by A4,A5,WAYBEL_0:def 38;
reconsider z = 0 as Element of N_5 by A2;
reconsider tj = 3\1 as Element of N_5 by A2;
reconsider dw = 2 as Element of N_5 by A2;
reconsider td = 3\2 as Element of N_5 by A2;
reconsider t = 3 as Element of N_5 by A2;
reconsider cl = the carrier of L as non empty set;
reconsider ck = the carrier of K as non empty set;
A7: ck = rng f by A4,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;
a in ck & b in ck & c in ck & d in ck & e in ck;
then reconsider A=a,B=b,C=c,D=d,E=e as Element of L;
take A,B,C,D,E;
thus A<>B by A6,Th4,WAYBEL_1:def 1;
thus A<>C by A6,WAYBEL_1:def 1;
thus A<>D by A6,Th3,WAYBEL_1:def 1;
thus A<>E by A6,WAYBEL_1:def 1;
now
assume f.td = f.dw;
then A8: td = dw by A5,A6,WAYBEL_1:def 1;
2 in td by Th4,TARSKI:def 1;
hence contradiction by A8;
end;
hence B<>C;
now
assume
A9: f.td = f.tj;
not 1 in td & 1 in tj by Th3,Th4,TARSKI:def 1,def 2;
hence contradiction by A5,A6,A9,WAYBEL_1:def 1;
end;
hence B<>D;
now
assume
A10: f.td = f.t;
not 1 in td & 1 in t by Th1,Th4,ENUMSET1:14,TARSKI:def 1;
hence contradiction by A5,A6,A10,WAYBEL_1:def 1;
end;
hence B<>E;
now
assume f.dw = f.tj;
then A11: dw = tj by A5,A6,WAYBEL_1:def 1;
2 in tj by Th3,TARSKI:def 2;
hence contradiction by A11;
end;
hence C<>D;
thus C<>E by A6,WAYBEL_1:def 1;
now
assume
A12: f.tj = f.t;
not 0 in tj & 0 in t by Th1,Th3,ENUMSET1:14,TARSKI:def 2;
hence contradiction by A5,A6,A12,WAYBEL_1:def 1;
end;
hence D<>E;
A13: {0, 3 \ 1, 2, 3 \ 2, 3} is non empty by ENUMSET1:24;
z c= td by XBOOLE_1:2;
then z <= td by A13,Def1,YELLOW_1:3;
then a <= b by A4,WAYBEL_0:66;
then A <= B by YELLOW_0:60;
hence A "/\" B = A by YELLOW_0:25;
z c= dw by XBOOLE_1:2;
then z <= dw by A13,Def1,YELLOW_1:3;
then a <= c by A4,WAYBEL_0:66;
then A <= C by YELLOW_0:60;
hence A "/\" C = A by YELLOW_0:25;
dw c= t by CARD_1:56;
then dw <= t by A13,Def1,YELLOW_1:3;
then c <= e by A4,WAYBEL_0:66;
then C <= E by YELLOW_0:60;
hence C"/\"E = C by YELLOW_0:25;
tj c= t by XBOOLE_1:36;
then tj <= t by A13,Def1,YELLOW_1:3;
then d <= e by A4,WAYBEL_0:66;
then D <= E by YELLOW_0:60;
hence D"/\"E = D by YELLOW_0:25;
thus B"/\"C = A
proof
B in the carrier of K & C in the carrier of K & 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 A7,YELLOW_0:40;
then consider x being set such that
A14: x in dom f & B"/\"C = f.x by FUNCT_1:def 5;
f is Function of the carrier of N_5,the carrier of K;
then dom f = the carrier of N_5 by FUNCT_2:def 1;
then reconsider x as Element of N_5 by A14;
A15: x = z or x = td or x = dw or x = tj or x = t by A1,ENUMSET1:23;
A16: now
assume B"/\"C = B;
then B <= C by YELLOW_0:25;
then b <= c by YELLOW_0:61;
then td <= dw by A4,WAYBEL_0:66;
then A17: td c= dw by A13,Def1,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
then 2 in 2 by A17;
hence contradiction;
end;
A18: now
assume B"/\"C = C;
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:61;
then dw <= td by A4,WAYBEL_0:66;
then A19: dw c= td by A13,Def1,YELLOW_1:3;
0 in dw & 0 <> 2 by CARD_5:1,TARSKI:def 2;
hence contradiction by A19,Th4,TARSKI:def 1;
end;
A20: now
assume B"/\"C = D;
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:61;
then tj <= dw by A4,WAYBEL_0:66;
then A21: tj c= dw by A13,Def1,YELLOW_1:3;
2 in tj by Th3,TARSKI:def 2;
then 2 in 2 by A21;
hence contradiction;
end;
now
assume B"/\"C = E;
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:61;
then t <= dw by A4,WAYBEL_0:66;
then A22: t c= dw by A13,Def1,YELLOW_1:3;
2 in t by Th1,ENUMSET1:14;
then 2 in 2 by A22;
hence contradiction;
end;
hence thesis by A14,A15,A16,A18,A20;
end;
td <= tj by A13,Def1,Lm1,YELLOW_1:3;
then b <= d by A4,WAYBEL_0:66;
then B <= D by YELLOW_0:60;
hence B"/\"D = B by YELLOW_0:25;
thus C"/\"D = A
proof
C in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:40;
then consider x being set such that
A23: x in dom f & C"/\"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of N_5,the carrier of K;
then dom f = the carrier of N_5 by FUNCT_2:def 1;
then reconsider x as Element of N_5 by A23;
A24: x = z or x = td or x = dw or x = tj or x = t by A1,ENUMSET1:23;
A25: now
assume C"/\"D = B;
then B <= C by YELLOW_0:23;
then b <= c by YELLOW_0:61;
then td <= dw by A4,WAYBEL_0:66;
then A26: td c= dw by A13,Def1,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
then 2 in 2 by A26;
hence contradiction;
end;
A27: now
assume C"/\"D = C;
then C <= D by YELLOW_0:25;
then c <= d by YELLOW_0:61;
then dw <= tj by A4,WAYBEL_0:66;
then A28: dw c= tj by A13,Def1,YELLOW_1:3;
0 in dw & 0 <> 2 & 0 <> 1 by CARD_5:1,TARSKI:def 2;
hence contradiction by A28,Th3,TARSKI:def 2;
end;
A29: now
assume C"/\"D = D;
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:61;
then tj <= dw by A4,WAYBEL_0:66;
then A30: tj c= dw by A13,Def1,YELLOW_1:3;
2 in tj by Th3,TARSKI:def 2;
then 2 in 2 by A30;
hence contradiction;
end;
now
assume C"/\"D = E;
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:61;
then t <= dw by A4,WAYBEL_0:66;
then A31: t c= dw by A13,Def1,YELLOW_1:3;
2 in t by Th1,ENUMSET1:14;
then 2 in 2 by A31;
hence contradiction;
end;
hence thesis by A23,A24,A25,A27,A29;
end;
thus B"\/"C = E
proof
B in the carrier of K & B in the carrier of K & 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 A7,YELLOW_0:41;
then consider x being set such that
A32: x in dom f & B"\/"C = f.x by FUNCT_1:def 5;
f is Function of the carrier of N_5,the carrier of K;
then dom f = the carrier of N_5 by FUNCT_2:def 1;
then reconsider x as Element of N_5 by A32;
A33: x = z or x = td or x = dw or x = tj or x = t by A1,ENUMSET1:23;
A34: now
assume B"\/"C = B;
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:61;
then td >= dw by A4,WAYBEL_0:66;
then A35: dw c= td by A13,Def1,YELLOW_1:3;
0 in dw & 0 <> 2 by CARD_5:1,TARSKI:def 2;
hence contradiction by A35,Th4,TARSKI:def 1;
end;
A36: now
assume B"\/"C = C;
then C >= B by YELLOW_0:24;
then c >= b by YELLOW_0:61;
then dw >= td by A4,WAYBEL_0:66;
then A37: td c= dw by A13,Def1,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
then 2 in 2 by A37;
hence contradiction;
end;
A38: now
assume B"\/"C = D;
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then tj >= dw by A4,WAYBEL_0:66;
then A39: dw c= tj by A13,Def1,YELLOW_1:3;
0 in dw & 0 <> 1 & 0 <>2 by CARD_5:1,TARSKI:def 2;
hence contradiction by A39,Th3,TARSKI:def 2;
end;
now
assume B"\/"C = A;
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:61;
then z >= dw by A4,WAYBEL_0:66;
then dw c= z by A13,Def1,YELLOW_1:3;
hence contradiction by XBOOLE_1:3;
end;
hence thesis by A32,A33,A34,A36,A38;
end;
thus C"\/"D = E
proof
C in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:41;
then consider x being set such that
A40: x in dom f & C"\/"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of N_5,the carrier of K;
then dom f = the carrier of N_5 by FUNCT_2:def 1;
then reconsider x as Element of N_5 by A40;
A41: x = z or x = td or x = dw or x = tj or x = t by A1,ENUMSET1:23;
A42: now
assume C"\/"D = B;
then B >= C by YELLOW_0:22;
then b >= c by YELLOW_0:61;
then td >= dw by A4,WAYBEL_0:66;
then A43: dw c= td by A13,Def1,YELLOW_1:3;
0 in dw & 0 <> 2 by CARD_5:1,TARSKI:def 2;
hence contradiction by A43,Th4,TARSKI:def 1;
end;
A44: now
assume C"\/"D = C;
then C >= D by YELLOW_0:24;
then c >= d by YELLOW_0:61;
then dw >= tj by A4,WAYBEL_0:66;
then A45: tj c= dw by A13,Def1,YELLOW_1:3;
2 in tj & 2 <> 0 & 2 <> 1 by Th3,TARSKI:def 2;
hence contradiction by A45,CARD_5:1,TARSKI:def 2;
end;
A46: now
assume C"\/"D = D;
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then tj >= dw by A4,WAYBEL_0:66;
then A47: dw c= tj by A13,Def1,YELLOW_1:3;
0 in dw & 0 <>1 & 0 <> 2 by CARD_5:1,TARSKI:def 2;
hence contradiction by A47,Th3,TARSKI:def 2;
end;
now
assume C"\/"D = A;
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:61;
then z >= dw by A4,WAYBEL_0:66;
then dw c= z by A13,Def1,YELLOW_1:3;
hence contradiction by XBOOLE_1:3;
end;
hence thesis by A40,A41,A42,A44,A46;
end;
end;
thus (ex a,b,c,d,e being Element of L st
(a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
A48: (a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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);
set ck = {a,b,c,d,e};
now
let x be set;
assume x in ck;
then x=a or x=b or x=c or x=d or x=e by ENUMSET1:23;
hence x in the carrier of L;
end;
then reconsider ck as Subset of L by TARSKI:def 3;
set K = subrelstr ck;
A49: the carrier of K = ck by YELLOW_0:def 15;
A50: a in ck by ENUMSET1:24;
A51: K is meet-inheriting
proof
let x,y be Element of L;
assume
A52: x in the carrier of K & y in the carrier of K & ex_inf_of {x,y},L;
per cases by A49,A52,ENUMSET1:23;
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 A49,ENUMSET1:24;
suppose x=a & y=b;
then inf{x,y} = a"/\"b by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=a & y=c;
then inf{x,y} = a"/\"c by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A53: x=a & y=d;
a <= b & b <= d by A48,YELLOW_0:25;
then a <= d by ORDERS_1:26;
then a"/\"d = a by YELLOW_0:25;
then inf {x,y} = a by A53,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose
A54: x=a & y=e;
a <= c & c <= e by A48,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then inf {x,y} = a by A54,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose x=b & y=a;
then inf{x,y} = a"/\"b by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose x=b & y=c;
then inf{x,y} = b"/\"c by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=b & y=d;
then inf{x,y} = b"/\"d by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A55: x=b & y=e;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e by ORDERS_1:26;
then b"/\"e = b by YELLOW_0:25;
then inf {x,y} = b by A55,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose x=c & y=a;
then inf{x,y} = a"/\"c by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=c & y=b;
then inf{x,y} = b"/\"c by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose x=c & y=d;
then inf{x,y} = c"/\"d by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=c & y=e;
then inf{x,y} = c"/\"e by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A56: x=d & y=a;
a <= b & b <= d by A48,YELLOW_0:25;
then a <= d by ORDERS_1:26;
then a"/\"d = a by YELLOW_0:25;
then inf {x,y} = a by A56,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose x=d & y=b;
then inf{x,y} = b"/\"d by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=d & y=c;
then inf{x,y} = c"/\"d by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose x=d & y=e;
then inf{x,y} = d"/\"e by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A57: x=e & y=a;
a <= c & c <= e by A48,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then inf {x,y} = a by A57,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose
A58: x=e & y=b;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e by ORDERS_1:26;
then b"/\"e = b by YELLOW_0:25;
then inf {x,y} = b by A58,YELLOW_0:40;
hence thesis by A49,ENUMSET1:24;
suppose x=e & y=c;
then inf{x,y} = c"/\"e by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
suppose x=e & y=d;
then inf{x,y} = d"/\"e by YELLOW_0:40;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
end;
K is join-inheriting
proof
let x,y be Element of L;
assume
A59: x in the carrier of K & y in the carrier of K & ex_sup_of {x,y},L;
per cases by A49,A59,ENUMSET1:23;
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 A49,ENUMSET1:24;
suppose x=a & y=b;
then x"\/"y = b by A48,Th5;
then sup{x,y} = b by YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose x=a & y=c;
then x"\/"y = c by A48,Th5;
then sup{x,y} = c by YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A60: x=a & y=d;
a <= b & b <= d by A48,YELLOW_0:25;
then a <= d by ORDERS_1:26;
then a"/\"d = a by YELLOW_0:25;
then a"\/"d = d by Th5;
then sup {x,y} = d by A60,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A61: x=a & y=e;
a <= c & c <= e by A48,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then a"\/"e = e by Th5;
then sup {x,y} = e by A61,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A62: x=b & y=a;
a"\/"b = b by A48,Th5;
then sup{x,y} = b by A62,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose x=b & y=c;
then sup{x,y} = b"\/"c by YELLOW_0:41;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A63: x=b & y=d;
b"\/"d = d by A48,Th5;
then sup{x,y} = d by A63,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A64: x=b & y=e;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e by ORDERS_1:26;
then b"/\"e = b by YELLOW_0:25;
then b"\/"e = e by Th5;
then sup {x,y} = e by A64,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A65: x=c & y=a;
c"\/"a = c by A48,Th5;
then sup{x,y} = c by A65,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose x=c & y=b;
then sup{x,y} = b"\/"c by YELLOW_0:41;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose x=c & y=d;
then sup{x,y} = c"\/"d by YELLOW_0:41;
hence thesis by A48,A49,ENUMSET1:24;
suppose
A66: x=c & y=e;
c"\/"e = e by A48,Th5;
then sup{x,y} = e by A66,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A67: x=d & y=a;
a <= b & b <= d by A48,YELLOW_0:25;
then a <= d by ORDERS_1:26;
then a"/\"d = a by YELLOW_0:25;
then a"\/"d = d by Th5;
then sup {x,y} = d by A67,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A68: x=d & y=b;
b"\/"d = d by A48,Th5;
then sup{x,y} = d by A68,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose x=d & y=c;
then sup{x,y} = c"\/"d by YELLOW_0:41;
hence thesis by A48,A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
suppose
A69: x=d & y=e;
d"\/"e = e by A48,Th5;
then sup{x,y} = e by A69,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A70: x=e & y=a;
a <= c & c <= e by A48,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then a"\/"e = e by Th5;
then sup {x,y} = e by A70,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A71: x=e & y=b;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e by ORDERS_1:26;
then b"/\"e = b by YELLOW_0:25;
then b"\/"e = e by Th5;
then sup {x,y} = e by A71,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A72: x=e & y=c;
c"\/"e = e by A48,Th5;
then sup{x,y} = e by A72,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
suppose
A73: x=e & y=d;
d"\/"e = e by A48,Th5;
then sup{x,y} = e by A73,YELLOW_0:41;
hence thesis by A49,ENUMSET1:24;
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 A49,ENUMSET1:24;
end;
then reconsider K as non empty full Sublattice of L
by A49,A50,A51,STRUCT_0:def 1;
take K;
thus N_5,K are_isomorphic
proof
reconsider z = 0 as Element of N_5 by A2;
reconsider tj = 3\1 as Element of N_5 by A2;
reconsider dw = 2 as Element of N_5 by A2;
reconsider td = 3\2 as Element of N_5 by A2;
reconsider t = 3 as Element of N_5 by A2;
A74: now
assume
A75: tj=dw;
2 in tj by Th3,TARSKI:def 2;
hence contradiction by A75;
end;
A76: now
assume
A77: tj=td;
not 1 in td & 1 in tj by Th3,Th4,TARSKI:def 1,def 2;
hence contradiction by A77;
end;
A78: now
assume
A79: tj=t;
not 0 in tj & 0 in t by Th1,Th3,ENUMSET1:14,TARSKI:def 2;
hence contradiction by A79;
end;
A80: now
assume
A81: dw=td; 2 in td by Th4,TARSKI:def 1;
hence contradiction by A81;
end;
A82: now
assume
A83: td=t;
not 1 in td & 1 in t by Th1,Th4,ENUMSET1:14,TARSKI:def 1;
hence contradiction by A83;
end;
defpred P[set,set] 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));
A84: for x being set st x in cn ex y being set st y in ck & P[x,y]
proof
let x be set;
assume
A85: x in cn;
per cases by A1,A85,ENUMSET1:23;
suppose
A86: x = 0;
take y=a;
thus y in ck by ENUMSET1:24;
let X be Element of N_5;
thus thesis by A86,Th3,Th4;
suppose
A87: x=3\1;
take y=d;
thus y in ck by ENUMSET1:24;
let X be Element of N_5;
thus thesis by A74,A76,A78,A87,Th3;
suppose
A88: x = 2;
take y=c;
thus y in ck by ENUMSET1:24;
let X be Element of N_5;
thus thesis by A74,A80,A88;
suppose
A89: x = 3 \ 2;
take y=b;
thus y in ck by ENUMSET1:24;
let X be Element of N_5;
thus thesis by A76,A80,A82,A89,Th4;
suppose
A90: x = 3;
take y=e;
thus y in ck by ENUMSET1:24;
let X be Element of N_5;
thus thesis by A78,A82,A90;
end;
consider f being Function of cn,ck such that
A91: for x being set st x in cn holds P[x,f.x] from FuncEx1(A84);
reconsider f as map of N_5,K by A49;
take f;
A92: f is one-to-one
proof
now
let x,y be Element of N_5;
assume
A93: f.x = f.y;
thus x=y
proof
per cases by A1,ENUMSET1:23;
suppose x = z & y = z;hence thesis;
suppose x = tj & y = tj;hence thesis;
suppose x = td & y = td;hence thesis;
suppose x = dw & y = dw;hence thesis;
suppose x = t & y = t;hence thesis;
suppose x = z & y = tj;
then f.x=a & f.y=d by A91;
hence thesis by A48,A93;
suppose x = z & y = dw;
then f.x=a & f.y=c by A91;
hence thesis by A48,A93;
suppose x = z & y = td;
then f.x=a & f.y=b by A91;
hence thesis by A48,A93;
suppose x = z & y = t;
then f.x=a & f.y=e by A91;
hence thesis by A48,A93;
suppose x = tj & y = z;
then f.x=d & f.y=a by A91;
hence thesis by A48,A93;
suppose x = tj & y = dw;
then f.x=d & f.y=c by A91;
hence thesis by A48,A93;
suppose x = tj & y = td;
then f.x=d & f.y=b by A91;
hence thesis by A48,A93;
suppose x = tj & y = t;
then f.x=d & f.y=e by A91;
hence thesis by A48,A93;
suppose x = dw & y = z;
then f.x=c & f.y=a by A91;
hence thesis by A48,A93;
suppose x = dw & y = tj;
then f.x=c & f.y=d by A91;
hence thesis by A48,A93;
suppose x = dw & y = td;
then f.x=c & f.y=b by A91;
hence thesis by A48,A93;
suppose x = dw & y = t;
then f.x=c & f.y=e by A91;
hence thesis by A48,A93;
suppose x = td & y = z;
then f.x=b & f.y=a by A91;
hence thesis by A48,A93;
suppose x = td & y = tj;
then f.x=b & f.y=d by A91;
hence thesis by A48,A93;
suppose x = td & y = dw;
then f.x=b & f.y=c by A91;
hence thesis by A48,A93;
suppose x = td & y = t;
then f.x=b & f.y=e by A91;
hence thesis by A48,A93;
suppose x = t & y = z;
then f.x=e & f.y=a by A91;
hence thesis by A48,A93;
suppose x = t & y = tj;
then f.x=e & f.y=d by A91;
hence thesis by A48,A93;
suppose x = t & y = dw;
then f.x=e & f.y=c by A91;
hence thesis by A48,A93;
suppose x = t & y = td;
then f.x=e & f.y=b by A91;
hence thesis by A48,A93;
end;
end;
hence thesis by WAYBEL_1:def 1;
end;
A94: dom f = the carrier of N_5 by FUNCT_2:def 1;
A95: rng f = ck
proof
thus rng f c= ck
proof
let y be set;
assume y in rng f;
then consider x being set such that
A96: x in dom f & y=f.x by FUNCT_1:def 5;
x in the carrier of N_5 by A96,FUNCT_2:def 1;
then reconsider x as Element of N_5;
(x = z or x = tj or x = dw or x = td or x = t) by A1,ENUMSET1:23;
then y=a or y=d or y=c or y=b or y=e by A91,A96;
hence thesis by ENUMSET1:24;
end;
thus ck c= rng f
proof
let y be set;
assume
A97: y in ck;
per cases by A97,ENUMSET1:23;
suppose
A98: y=a;
z in dom f & a = f.z by A91,A94;
hence y in rng f by A98,FUNCT_1:def 5;
suppose
A99: y=b;
td in dom f & b=f.td by A91,A94;
hence y in rng f by A99,FUNCT_1:def 5;
suppose
A100: y=c;
dw in dom f & c = f.dw by A91,A94;
hence y in rng f by A100,FUNCT_1:def 5;
suppose
A101: y=d;
tj in dom f & d=f.tj by A91,A94;
hence y in rng f by A101,FUNCT_1:def 5;
suppose
A102: y=e;
t in dom f & e=f.t by A91,A94;
hence y in rng f by A102,FUNCT_1:def 5;
end;
end;
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;
A103: {0, 3 \ 1, 2, 3 \ 2, 3} is non empty by ENUMSET1:24;
thus x <= y implies f.x <= f.y
proof
assume
A104: x <= y;
per cases by A1,ENUMSET1:23;
suppose x=z & y=z;hence thesis;
suppose x=z & y=td;
then A105: f.x = a & f.y = b by A91;
a in the carrier of K & b in the carrier of K by A49,ENUMSET1:24;
then reconsider A=a,B=b as Element of K;
a <= b & A in the carrier of K & B in the carrier of K
by A48,YELLOW_0:25;
hence f.x <= f.y by A105,YELLOW_0:61;
suppose x=z & y=dw;
then A106: f.x = a & f.y = c by A91;
a in the carrier of K & c in the carrier of K by A49,ENUMSET1:24;
then reconsider A=a,C=c as Element of K;
a <= c & A in the carrier of K & C in the carrier of K
by A48,YELLOW_0:25;
hence f.x <= f.y by A106,YELLOW_0:61;
suppose x=z & y=tj;
then A107: f.x = a & f.y = d by A91;
a in the carrier of K & d in the carrier of K by A49,ENUMSET1:24;
then reconsider A=a,D=d as Element of K;
a <= b & b <= d by A48,YELLOW_0:25;
then a <= d & A in the carrier of K & D in the carrier of K
by ORDERS_1:26;
hence f.x <= f.y by A107,YELLOW_0:61;
suppose x=z & y=t;
then A108: f.x = a & f.y = e by A91;
a in the carrier of K & e in the carrier of K by A49,ENUMSET1:24;
then reconsider A=a,E=e as Element of K;
a <= c & c <= e by A48,YELLOW_0:25;
then a <= e & A in the carrier of K & E in the carrier of K
by ORDERS_1:26;
hence f.x <= f.y by A108,YELLOW_0:61;
suppose x=td & y=z;
then td c= z by A103,A104,Def1,YELLOW_1:3;
hence thesis by Th4,XBOOLE_1:3;
suppose x=td & y=td;hence thesis;
suppose
A109: x=td & y=dw;
2 in td & not 2 in dw by Th4,TARSKI:def 1;
then not td c= dw;
hence thesis by A103,A104,A109,Def1,YELLOW_1:3;
suppose x=td & y=z;
then td c= z by A103,A104,Def1,YELLOW_1:3;
hence thesis by Th4,XBOOLE_1:3;
suppose x=td & y=tj;
then A110: f.x = b & f.y = d by A91;
b in the carrier of K & d in the carrier of K by A49,ENUMSET1:24;
then reconsider D=d,B=b as Element of K;
b <= d & B in the carrier of K & D in the carrier of K
by A48,YELLOW_0:25;
hence f.x <= f.y by A110,YELLOW_0:61;
suppose x=td & y=t;
then A111: f.x = b & f.y = e by A91;
b in the carrier of K & e in the carrier of K by A49,ENUMSET1:24;
then reconsider B=b,E=e as Element of K;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e & B in the carrier of K & E in the carrier of K
by ORDERS_1:26;
hence f.x <= f.y by A111,YELLOW_0:61;
suppose x=dw & y=z;
then dw c= z by A103,A104,Def1,YELLOW_1:3;
hence thesis by XBOOLE_1:3;
suppose
A112: x=dw & y=td;
0 in dw & not 0 in td by Th4,CARD_5:1,TARSKI:def 1,def 2;
then not dw c= td;
hence thesis by A103,A104,A112,Def1,YELLOW_1:3;
suppose x=dw & y=dw;hence thesis;
suppose
A113: x=dw & y=tj;
0 in dw & not 0 in tj by Th3,CARD_5:1,TARSKI:def 2;
then not dw c= tj;
hence thesis by A103,A104,A113,Def1,YELLOW_1:3;
suppose x=dw & y=t;
then A114: f.x = c & f.y = e by A91;
c in the carrier of K & e in the carrier of K by A49,ENUMSET1:24;
then reconsider C=c,E=e as Element of K;
c <= e & C in the carrier of K & E in the carrier of K
by A48,YELLOW_0:25;
hence f.x <= f.y by A114,YELLOW_0:61;
suppose x=tj & y=z;
then tj c= z by A103,A104,Def1,YELLOW_1:3;
hence thesis by Th3,XBOOLE_1:3;
suppose
A115: x=tj & y=td;
1 in tj & not 1 in td by Th3,Th4,TARSKI:def 1,def 2;
then not tj c= td;
hence thesis by A103,A104,A115,Def1,YELLOW_1:3;
suppose
A116: x=tj & y=dw;
2 in tj & not 2 in dw by Th3,TARSKI:def 2;
then not tj c= dw;
hence thesis by A103,A104,A116,Def1,YELLOW_1:3;
suppose x=tj & y=tj;hence thesis;
suppose x=tj & y=t;
then A117: f.x = d & f.y = e by A91;
d in the carrier of K & e in the carrier of K by A49,ENUMSET1:24;
then reconsider D=d,E=e as Element of K;
d <= e & D in the carrier of K & E in the carrier of K
by A48,YELLOW_0:25;
hence f.x <= f.y by A117,YELLOW_0:61;
suppose x=t & y=z;
then t c= z by A103,A104,Def1,YELLOW_1:3;
hence thesis by XBOOLE_1:3;
suppose
A118: x=t & y=td;
0 in t & not 0 in td by Th1,Th4,ENUMSET1:14,TARSKI:def 1;
then not t c= td;
hence thesis by A103,A104,A118,Def1,YELLOW_1:3;
suppose
A119: x=t & y=dw;
2 in t & not 2 in dw by Th1,ENUMSET1:14;
then not t c= dw;
hence thesis by A103,A104,A119,Def1,YELLOW_1:3;
suppose
A120: x=t & y=tj;
0 in t & not 0 in tj by Th1,Th3,ENUMSET1:14,TARSKI:def 2;
then not t c= tj;
hence thesis by A103,A104,A120,Def1,YELLOW_1:3;
suppose x=t & y=t;hence thesis;
end;
thus f.x <= f.y implies x <= y
proof
assume
A121: f.x <= f.y;
A122: f.x in ck & f.y in ck by A94,A95,FUNCT_1:def 5;
per cases by A122,ENUMSET1:23;
suppose f.x = a & f.y = a;
hence x <= y by A92,WAYBEL_1:def 1;
suppose A123: f.x = a & f.y = b;
f.z = a & f.td = b by A91;
then z=x & td = y by A92,A123,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A103,Def1,YELLOW_1:3;
suppose A124: f.x = a & f.y = c;
f.z = a & f.dw = c by A91;
then z=x & dw = y by A92,A124,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A103,Def1,YELLOW_1:3;
suppose A125: f.x = a & f.y = d;
f.z = a & f.tj = d by A91;
then z=x & tj = y by A92,A125,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A103,Def1,YELLOW_1:3;
suppose A126: f.x = a & f.y = e;
f.z = a & f.t = e by A91;
then z=x & t = y by A92,A126,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A103,Def1,YELLOW_1:3;
suppose f.x = b & f.y = a;
then b <= a by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = b & f.y = b;
hence x <= y by A92,WAYBEL_1:def 1;
suppose f.x = b & f.y = c;
then b <= c by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose A127: f.x = b & f.y = d;
f.td = b & f.tj = d by A91;
then x=td & y=tj & 1 c= 2 by A92,A127,CARD_1:56,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:34;
hence x <= y by A103,Def1,YELLOW_1:3;
suppose A128: f.x = b & f.y = e;
A129: td c= t
proof
let X be set;
assume X in td;
then X = 2 by Th4,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
f.td = b & f.t = e by A91;
then td=x & t = y by A92,A128,WAYBEL_1:def 1;
hence x <= y by A103,A129,Def1,YELLOW_1:3;
suppose f.x = c & f.y = a;
then c <= a by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = c & f.y = b;
then c <= b by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = c & f.y = c;
hence x <= y by A92,WAYBEL_1:def 1;
suppose f.x = c & f.y = d;
then c <= d by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose A130: f.x = c & f.y = e;
A131: dw c= t
proof
let X be set;
assume X in dw;
then X=0 or X=1 by CARD_5:1,TARSKI:def 2;
hence thesis by Th1,ENUMSET1:14;
end;
f.dw = c & f.t = e by A91;
then dw=x & t = y by A92,A130,WAYBEL_1:def 1;
hence x <= y by A103,A131,Def1,YELLOW_1:3;
suppose f.x = d & f.y = a;
then d <= a & a <= b by A48,A121,YELLOW_0:25,60;
then d <= b by ORDERS_1:26;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = d & f.y = b;
then d <= b by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = d & f.y = c;
then d <= c by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = d & f.y = d;
hence x <= y by A92,WAYBEL_1:def 1;
suppose A132: f.x = d & f.y = e;
A133: tj c= t
proof
let X be set;
assume X in tj;
then X=2 or X=1 by Th3,TARSKI:def 2;
hence thesis by Th1,ENUMSET1:14;
end;
f.tj = d & f.t = e by A91;
then tj=x & t = y by A92,A132,WAYBEL_1:def 1;
hence x <= y by A103,A133,Def1,YELLOW_1:3;
suppose f.x = e & f.y = a;
then A134: e <= a by A121,YELLOW_0:60;
a <= b & b <= d & d <= e by A48,YELLOW_0:25;
then a <= d & d <= e by ORDERS_1:26;
then a <= e by ORDERS_1:26;
hence x <= y by A48,A134,ORDERS_1:25;
suppose f.x = e & f.y = b;
then A135: e <= b by A121,YELLOW_0:60;
b <= d & d <= e by A48,YELLOW_0:25;
then b <= e by ORDERS_1:26;
hence x <= y by A48,A135,ORDERS_1:25;
suppose f.x = e & f.y = c;
then e <= c by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = e & f.y = d;
then e <= d by A121,YELLOW_0:60;
hence x <= y by A48,YELLOW_0:25;
suppose f.x = e & f.y = e;
hence x <= y by A92,WAYBEL_1:def 1;
end;
end;
hence f is isomorphic by A49,A92,A95,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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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;
set cn = the carrier of M_3;
A1: cn = {0, 1, 2 \ 1 , 3 \ 2, 3} by Def2,YELLOW_1:1;
then A2: 0 in cn & 1 in cn & 2\1 in cn & 3\2 in cn & 3 in cn by ENUMSET1:24;
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
given K being full Sublattice of L such that
A3: M_3,K are_isomorphic;
consider f being map of M_3,K such that
A4: f is isomorphic by A3,WAYBEL_1:def 8;
A5: K is non empty by A4,WAYBEL_0:def 38;
reconsider K as non empty SubRelStr of L by A4,WAYBEL_0:def 38;
A6: f is one-to-one monotone by A4,A5,WAYBEL_0:def 38;
reconsider z = 0 as Element of M_3 by A2;
reconsider j = 1 as Element of M_3 by A2;
reconsider dj = 2\1 as Element of M_3 by A2;
reconsider td = 3\2 as Element of M_3 by A2;
reconsider t = 3 as Element of M_3 by A2;
reconsider cl = the carrier of L as non empty set;
reconsider ck = the carrier of K as non empty set;
A7: ck = rng f by A4,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;
a in ck & b in ck & c in ck & d in ck & e in ck;
then reconsider A=a,B=b,C=c,D=d,E=e as Element of L;
take A,B,C,D,E;
thus A<>B by A6,WAYBEL_1:def 1;
thus A<>C by A6,Th2,WAYBEL_1:def 1;
thus A<>D by A6,Th4,WAYBEL_1:def 1;
thus A<>E by A6,WAYBEL_1:def 1;
now
assume f.j = f.dj;
then j = dj by A5,A6,WAYBEL_1:def 1;
then 1 in 1 by Th2,TARSKI:def 1;
hence contradiction;
end;
hence B<>C;
now
assume f.j = f.td;
then A8: j = td by A5,A6,WAYBEL_1:def 1;
0 in j & 0 <> 2 by CARD_5:1,TARSKI:def 1;
hence contradiction by A8,Th4,TARSKI:def 1;
end;
hence B<>D;
thus B<>E by A6,WAYBEL_1:def 1;
now
assume f.dj = f.td;
then A9: dj = td by A5,A6,WAYBEL_1:def 1;
1 in dj & 1 <> 2 by Th2,TARSKI:def 1;
hence contradiction by A9,Th4,TARSKI:def 1;
end;
hence C<>D;
now
assume f.dj = f.t;
then A10: dj = t by A5,A6,WAYBEL_1:def 1;
0 in t & 0 <> 1 by Th1,ENUMSET1:14;
hence contradiction by A10,Th2,TARSKI:def 1;
end;
hence C<>E;
now
assume f.td = f.t;
then A11: td = t by A5,A6,WAYBEL_1:def 1;
0 in t & 0 <> 2 by Th1,ENUMSET1:14;
hence contradiction by A11,Th4,TARSKI:def 1;
end;
hence D<>E;
A12: {0, 1, 2 \ 1 , 3 \ 2, 3} is non empty by ENUMSET1:24;
z c= j by XBOOLE_1:2;
then z <= j by A12,Def2,YELLOW_1:3;
then a <= b by A4,WAYBEL_0:66;
then A <= B by YELLOW_0:60;
hence A "/\" B = A by YELLOW_0:25;
z c= dj by XBOOLE_1:2;
then z <= dj by A12,Def2,YELLOW_1:3;
then a <= c by A4,WAYBEL_0:66;
then A <= C by YELLOW_0:60;
hence A "/\" C = A by YELLOW_0:25;
z c= td by XBOOLE_1:2;
then z <= td by A12,Def2,YELLOW_1:3;
then a <= d by A4,WAYBEL_0:66;
then A <= D by YELLOW_0:60;
hence A "/\" D = A by YELLOW_0:25;
j c= t by CARD_1:56;
then j <= t by A12,Def2,YELLOW_1:3;
then b <= e by A4,WAYBEL_0:66;
then B <= E by YELLOW_0:60;
hence B "/\" E = B by YELLOW_0:25;
dj c= t
proof
let x be set;
assume x in dj; then x=1 by Th2,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then dj <= t by A12,Def2,YELLOW_1:3;
then c <= e by A4,WAYBEL_0:66;
then C <= E by YELLOW_0:60;
hence C"/\"E = C by YELLOW_0:25;
td c= t
proof
let x be set;
assume x in td; then x=2 by Th4,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
then td <= t by A12,Def2,YELLOW_1:3;
then d <= e by A4,WAYBEL_0:66;
then D <= E by YELLOW_0:60;
hence D"/\"E = D by YELLOW_0:25;
thus B"/\"C = A
proof
B in the carrier of K & C in the carrier of K & 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 A7,YELLOW_0:40;
then consider x being set such that
A13: x in dom f & B"/\"C = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A13;
A14: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A15: now
assume B"/\"C = B;
then B <= C by YELLOW_0:25;
then b <= c by YELLOW_0:61;
then j <= dj by A4,WAYBEL_0:66;
then A16: j c= dj by A12,Def2,YELLOW_1:3;
0 in j by CARD_5:1,TARSKI:def 1;
hence contradiction by A16,Th2,TARSKI:def 1;
end;
A17: now
assume B"/\"C = C;
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:61;
then dj <= j by A4,WAYBEL_0:66;
then A18: dj c= j by A12,Def2,YELLOW_1:3;
1 in dj & 0 <> 1 by Th2,TARSKI:def 1;
hence contradiction by A18,CARD_5:1,TARSKI:def 1;
end;
A19: now
assume B"/\"C = D;
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:61;
then td <= dj by A4,WAYBEL_0:66;
then A20: td c= dj by A12,Def2,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
hence contradiction by A20,Th2,TARSKI:def 1;
end;
now
assume B"/\"C = E;
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:61;
then t <= dj by A4,WAYBEL_0:66;
then A21: t c= dj by A12,Def2,YELLOW_1:3;
2 in t by Th1,ENUMSET1:14;
hence contradiction by A21,Th2,TARSKI:def 1;
end;
hence thesis by A13,A14,A15,A17,A19;
end;
thus B"/\"D = A
proof
B in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:40;
then consider x being set such that
A22: x in dom f & B"/\"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A22;
A23: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A24: now
assume B"/\"D = B;
then B <= D by YELLOW_0:25;
then b <= d by YELLOW_0:61;
then j <= td by A4,WAYBEL_0:66;
then A25: j c= td by A12,Def2,YELLOW_1:3;
0 in j by CARD_5:1,TARSKI:def 1;
hence contradiction by A25,Th4,TARSKI:def 1;
end;
A26: now
assume B"/\"D = C;
then C <= B by YELLOW_0:23;
then c <= b by YELLOW_0:61;
then dj <= j by A4,WAYBEL_0:66;
then A27: dj c= j by A12,Def2,YELLOW_1:3;
1 in dj & 0 <> 1 by Th2,TARSKI:def 1;
hence contradiction by A27,CARD_5:1,TARSKI:def 1;
end;
A28: now
assume B"/\"D = D;
then D <= B by YELLOW_0:23;
then d <= b by YELLOW_0:61;
then td <= j by A4,WAYBEL_0:66;
then A29: td c= j by A12,Def2,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
hence contradiction by A29,CARD_5:1,TARSKI:def 1;
end;
now
assume B"/\"D = E;
then E <= B by YELLOW_0:23;
then e <= b by YELLOW_0:61;
then t <= j by A4,WAYBEL_0:66;
then A30: t c= j by A12,Def2,YELLOW_1:3;
2 in t by Th1,ENUMSET1:14;
hence contradiction by A30,CARD_5:1,TARSKI:def 1;
end;
hence thesis by A22,A23,A24,A26,A28;
end;
thus C"/\"D = A
proof
C in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:40;
then consider x being set such that
A31: x in dom f & C"/\"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A31;
A32: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A33: now
assume C"/\"D = B;
then B <= C by YELLOW_0:23;
then b <= c by YELLOW_0:61;
then j <= dj by A4,WAYBEL_0:66;
then A34: j c= dj by A12,Def2,YELLOW_1:3;
0 in j by CARD_5:1,TARSKI: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:61;
then dj <= td by A4,WAYBEL_0:66;
then A36: dj c= td by A12,Def2,YELLOW_1:3;
1 in dj & 1 <> 2 by Th2,TARSKI:def 1;
hence contradiction by A36,Th4,TARSKI:def 1;
end;
A37: now
assume C"/\"D = D;
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:61;
then td <= dj by A4,WAYBEL_0:66;
then A38: td c= dj by A12,Def2,YELLOW_1:3;
2 in td by Th4,TARSKI:def 1;
hence contradiction by A38,Th2,TARSKI:def 1;
end;
now
assume C"/\"D = E;
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:61;
then t <= dj by A4,WAYBEL_0:66;
then A39: t c= dj by A12,Def2,YELLOW_1:3;
2 in t by Th1,ENUMSET1:14;
hence contradiction by A39,Th2,TARSKI:def 1;
end;
hence thesis by A31,A32,A33,A35,A37;
end;
thus B"\/"C = E
proof
B in the carrier of K & B in the carrier of K & 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 A7,YELLOW_0:41;
then consider x being set such that
A40: x in dom f & B"\/"C = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A40;
A41: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A42: now
assume B"\/"C = B;
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:61;
then j >= dj by A4,WAYBEL_0:66;
then A43: dj c= j by A12,Def2,YELLOW_1:3;
1 in dj & 0 <> 1 by Th2,TARSKI:def 1;
hence contradiction by A43,CARD_5:1,TARSKI:def 1;
end;
A44: now
assume B"\/"C = C;
then C >= B by YELLOW_0:24;
then c >= b by YELLOW_0:61;
then dj >= j by A4,WAYBEL_0:66;
then A45: j c= dj by A12,Def2,YELLOW_1:3;
0 in j by CARD_5:1,TARSKI:def 1;
hence contradiction by A45,Th2,TARSKI:def 1;
end;
A46: now
assume B"\/"C = D;
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then td >= dj by A4,WAYBEL_0:66;
then A47: dj c= td by A12,Def2,YELLOW_1:3;
1 in dj & 2 <> 1 by Th2,TARSKI:def 1;
hence contradiction by A47,Th4,TARSKI:def 1;
end;
now
assume B"\/"C = A;
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:61;
then z >= dj by A4,WAYBEL_0:66;
then dj c= z by A12,Def2,YELLOW_1:3;
hence contradiction by Th2,XBOOLE_1:3;
end;
hence thesis by A40,A41,A42,A44,A46;
end;
thus B"\/"D = E
proof
B in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:41;
then consider x being set such that
A48: x in dom f & B"\/"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A48;
A49: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A50: now
assume B"\/"D = B;
then B >= D by YELLOW_0:22;
then b >= d by YELLOW_0:61;
then j >= td by A4,WAYBEL_0:66;
then A51: td c= j by A12,Def2,YELLOW_1:3;
2 in td & 2 <> 0 by Th4,TARSKI:def 1;
hence contradiction by A51,CARD_5:1,TARSKI:def 1;
end;
A52: now
assume B"\/"D = C;
then C >= D by YELLOW_0:22;
then c >= d by YELLOW_0:61;
then dj >= td by A4,WAYBEL_0:66;
then A53: td c= dj by A12,Def2,YELLOW_1:3;
2 in td & 2 <> 1 by Th4,TARSKI:def 1;
hence contradiction by A53,Th2,TARSKI:def 1;
end;
A54: now
assume B"\/"D = D;
then D >= B by YELLOW_0:22;
then d >= b by YELLOW_0:61;
then td >= j by A4,WAYBEL_0:66;
then A55: j c= td by A12,Def2,YELLOW_1:3;
0 in j & 0 <> 2 by CARD_5:1,TARSKI:def 1;
hence contradiction by A55,Th4,TARSKI:def 1;
end;
now
assume B"\/"D = A;
then A >= B by YELLOW_0:22;
then a >= b by YELLOW_0:61;
then z >= j by A4,WAYBEL_0:66;
then j c= z by A12,Def2,YELLOW_1:3;
hence contradiction by XBOOLE_1:3;
end;
hence thesis by A48,A49,A50,A52,A54;
end;
thus C"\/"D = E
proof
C in the carrier of K & D in the carrier of K & 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 A7,YELLOW_0:41;
then consider x being set such that
A56: x in dom f & C"\/"D = f.x by FUNCT_1:def 5;
f is Function of the carrier of M_3,the carrier of K;
then dom f = the carrier of M_3 by FUNCT_2:def 1;
then reconsider x as Element of M_3 by A56;
A57: x = z or x = j or x = dj or x = td or x = t by A1,ENUMSET1:23;
A58: now
assume C"\/"D = B;
then B >= C by YELLOW_0:22;
then b >= c by YELLOW_0:61;
then j >= dj by A4,WAYBEL_0:66;
then A59: dj c= j by A12,Def2,YELLOW_1:3;
1 in dj by Th2,TARSKI:def 1;
then 1 in 1 by A59;
hence contradiction;
end;
A60: now
assume C"\/"D = C;
then C >= D by YELLOW_0:24;
then c >= d by YELLOW_0:61;
then dj >= td by A4,WAYBEL_0:66;
then A61: td c= dj by A12,Def2,YELLOW_1:3;
2 in td & 2 <> 1 by Th4,TARSKI:def 1;
hence contradiction by A61,Th2,TARSKI:def 1;
end;
A62: now
assume C"\/"D = D;
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then td >= dj by A4,WAYBEL_0:66;
then A63: dj c= td by A12,Def2,YELLOW_1:3;
1 in dj & 1 <> 2 by Th2,TARSKI:def 1;
hence contradiction by A63,Th4,TARSKI:def 1;
end;
now
assume C"\/"D = A;
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:61;
then z >= dj by A4,WAYBEL_0:66;
then dj c= z by A12,Def2,YELLOW_1:3;
hence contradiction by Th2,XBOOLE_1:3;
end;
hence thesis by A56,A57,A58,A60,A62;
end;
end;
thus (ex a,b,c,d,e being Element of L st
(a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
A64: a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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;
set ck = {a,b,c,d,e};
now
let x be set;
assume x in ck;
then x=a or x=b or x=c or x=d or x=e by ENUMSET1:23;
hence x in the carrier of L;
end;
then reconsider ck as Subset of L by TARSKI:def 3;
set K = subrelstr ck;
A65: the carrier of K = ck by YELLOW_0:def 15;
A66: a in ck by ENUMSET1:24;
A67: K is meet-inheriting
proof
let x,y be Element of L;
assume
A68: x in the carrier of K & y in the carrier of K & ex_inf_of {x,y},L;
per cases by A65,A68,ENUMSET1:23;
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 A65,ENUMSET1:24;
suppose x=a & y=b;
then inf{x,y} = a"/\"b by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=a & y=c;
then inf{x,y} = a"/\"c by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=a & y=d;
then inf{x,y} = a"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose
A69: x=a & y=e;
a <= c & c <= e by A64,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then inf {x,y} = a by A69,YELLOW_0:40;
hence thesis by A65,ENUMSET1:24;
suppose x=b & y=a;
then inf{x,y} = a"/\"b by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose x=b & y=c;
then inf{x,y} = b"/\"c by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=b & y=d;
then inf{x,y} = b"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=b & y=e;
then inf{x,y} = b"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=c & y=a;
then inf{x,y} = a"/\"c by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=c & y=b;
then inf{x,y} = b"/\"c by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose x=c & y=d;
then inf{x,y} = c"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=c & y=e;
then inf{x,y} = c"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=d & y=a;
then inf{x,y} = a"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=d & y=b;
then inf{x,y} = b"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=d & y=c;
then inf{x,y} = c"/\"d by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose x=d & y=e;
then inf{x,y} = d"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose
A70: x=e & y=a;
a <= c & c <= e by A64,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then inf {x,y} = a by A70,YELLOW_0:40;
hence thesis by A65,ENUMSET1:24;
suppose x=e & y=b;
then inf{x,y} = b"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=e & y=c;
then inf{x,y} = c"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=e & y=d;
then inf{x,y} = d"/\"e by YELLOW_0:40;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
end;
K is join-inheriting
proof
let x,y be Element of L;
assume
A71: x in the carrier of K & y in the carrier of K & ex_sup_of {x,y},L;
per cases by A65,A71,ENUMSET1:23;
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 A65,ENUMSET1:24;
suppose x=a & y=b;
then x"\/"y = b by A64,Th5;
then sup{x,y} = b by YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose x=a & y=c;
then x"\/"y = c by A64,Th5;
then sup{x,y} = c by YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose x=a & y=d;
then x"\/"y = d by A64,Th5;
then sup{x,y} = d by YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A72: x=a & y=e;
a <= c & c <= e by A64,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then a"\/"e = e by Th5;
then sup {x,y} = e by A72,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A73: x=b & y=a;
a"\/"b = b by A64,Th5;
then sup{x,y} = b by A73,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose x=b & y=c;
then sup{x,y} = b"\/"c by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=b & y=d;
then sup{x,y} = b"\/"d by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
suppose
A74: x=b & y=e;
b"\/"e = e by A64,Th5;
then sup{x,y} = e by A74,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A75: x=c & y=a;
c"\/"a = c by A64,Th5;
then sup{x,y} = c by A75,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose x=c & y=b;
then sup{x,y} = b"\/"c by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose x=c & y=d;
then sup{x,y} = c"\/"d by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
suppose
A76: x=c & y=e;
c"\/"e = e by A64,Th5;
then sup{x,y} = e by A76,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose x=d & y=a;
then x"\/"y = d by A64,Th5;
then sup{x,y} = d by YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose x=d & y=b;
then sup{x,y} = b"\/"d by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
suppose x=d & y=c;
then sup{x,y} = c"\/"d by YELLOW_0:41;
hence thesis by A64,A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
suppose
A77: x=d & y=e;
d"\/"e = e by A64,Th5;
then sup{x,y} = e by A77,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A78: x=e & y=a;
a <= c & c <= e by A64,YELLOW_0:25;
then a <= e by ORDERS_1:26;
then a"/\"e = a by YELLOW_0:25;
then a"\/"e = e by Th5;
then sup {x,y} = e by A78,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A79: x=e & y=b;
b"\/"e = e by A64,Th5;
then sup{x,y} = e by A79,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A80: x=e & y=c;
c"\/"e = e by A64,Th5;
then sup{x,y} = e by A80,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
suppose
A81: x=e & y=d;
d"\/"e = e by A64,Th5;
then sup{x,y} = e by A81,YELLOW_0:41;
hence thesis by A65,ENUMSET1:24;
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 A65,ENUMSET1:24;
end;
then reconsider K as non empty full Sublattice of L
by A65,A66,A67,STRUCT_0:def 1;
take K;
thus M_3,K are_isomorphic
proof
reconsider z = 0 as Element of M_3 by A2;
reconsider j = 1 as Element of M_3 by A2;
reconsider dj = 2\1 as Element of M_3 by A2;
reconsider td = 3\2 as Element of M_3 by A2;
reconsider t = 3 as Element of M_3 by A2;
A82: now
assume
A83: j=dj;
1 in dj by Th2,TARSKI:def 1;
hence contradiction by A83;
end;
A84: now
assume
A85: j=td;
2 in td & 0 <> 2 by Th4,TARSKI:def 1;
hence contradiction by A85,CARD_5:1,TARSKI:def 1;
end;
A86: now
assume
A87: dj=td;
2 in td & 1 <> 2 by Th4,TARSKI:def 1;
hence contradiction by A87,Th2,TARSKI:def 1;
end;
A88: now
assume
A89: dj=t;
2 in t & 1 <> 2 by Th1,ENUMSET1:14;
hence contradiction by A89,Th2,TARSKI:def 1;
end;
A90: now
assume
A91: td=t;
0 in t & 0 <> 2 by Th1,ENUMSET1:14;
hence contradiction by A91,Th4,TARSKI:def 1;
end;
defpred P[set,set] 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));
A92: for x being set st x in cn ex y being set st y in ck & P[x,y]
proof
let x be set;
assume
A93: x in cn;
per cases by A1,A93,ENUMSET1:23;
suppose
A94: x = 0;
take y=a;
thus y in ck by ENUMSET1:24;
let X be Element of M_3;
thus thesis by A94,Th2,Th4;
suppose
A95: x=1;
take y=b;
thus y in ck by ENUMSET1:24;
let X be Element of M_3;
thus thesis by A82,A84,A95;
suppose
A96: x = 2\1;
take y=c;
thus y in ck by ENUMSET1:24;
let X be Element of M_3;
thus thesis by A82,A86,A88,A96,Th2;
suppose
A97: x = 3 \ 2;
take y=d;
thus y in ck by ENUMSET1:24;
let X be Element of M_3;
thus thesis by A84,A86,A90,A97,Th4;
suppose
A98: x = 3;
take y=e;
thus y in ck by ENUMSET1:24;
let X be Element of M_3;
thus thesis by A88,A90,A98;
end;
consider f being Function of cn,ck such that
A99: for x being set st x in cn holds P[x,f.x] from FuncEx1(A92);
reconsider f as map of M_3,K by A65;
take f;
A100: f is one-to-one
proof
now
let x,y be Element of M_3;
assume
A101: f.x = f.y;
thus x=y
proof
per cases by A1,ENUMSET1:23;
suppose x = z & y = z;hence thesis;
suppose x = j & y = j;hence thesis;
suppose x = dj & y = dj;hence thesis;
suppose x = td & y = td;hence thesis;
suppose x = t & y = t;hence thesis;
suppose x = z & y = j;
then f.x=a & f.y=b by A99;
hence thesis by A64,A101;
suppose x = z & y = dj;
then f.x=a & f.y=c by A99;
hence thesis by A64,A101;
suppose x = z & y = td;
then f.x=a & f.y=d by A99;
hence thesis by A64,A101;
suppose x = z & y = t;
then f.x=a & f.y=e by A99;
hence thesis by A64,A101;
suppose x = j & y = z;
then f.x=b & f.y=a by A99;
hence thesis by A64,A101;
suppose x = j & y = dj;
then f.x=b & f.y=c by A99;
hence thesis by A64,A101;
suppose x = j & y = td;
then f.x=b & f.y=d by A99;
hence thesis by A64,A101;
suppose x = j & y = t;
then f.x=b & f.y=e by A99;
hence thesis by A64,A101;
suppose x = dj & y = z;
then f.x=c & f.y=a by A99;
hence thesis by A64,A101;
suppose x = dj & y = j;
then f.x=c & f.y=b by A99;
hence thesis by A64,A101;
suppose x = dj & y = td;
then f.x=c & f.y=d by A99;
hence thesis by A64,A101;
suppose x = dj & y = t;
then f.x=c & f.y=e by A99;
hence thesis by A64,A101;
suppose x = td & y = z;
then f.x=d & f.y=a by A99;
hence thesis by A64,A101;
suppose x = td & y = j;
then f.x=d & f.y=b by A99;
hence thesis by A64,A101;
suppose x = td & y = dj;
then f.x=d & f.y=c by A99;
hence thesis by A64,A101;
suppose x = td & y = t;
then f.x=d & f.y=e by A99;
hence thesis by A64,A101;
suppose x = t & y = z;
then f.x=e & f.y=a by A99;
hence thesis by A64,A101;
suppose x = t & y = j;
then f.x=e & f.y=b by A99;
hence thesis by A64,A101;
suppose x = t & y = dj;
then f.x=e & f.y=c by A99;
hence thesis by A64,A101;
suppose x = t & y = td;
then f.x=e & f.y=d by A99;
hence thesis by A64,A101;
end;
end;
hence thesis by WAYBEL_1:def 1;
end;
A102: dom f = the carrier of M_3 by FUNCT_2:def 1;
A103: rng f = ck
proof
thus rng f c= ck
proof
let y be set;
assume y in rng f;
then consider x being set such that
A104: x in dom f & y=f.x by FUNCT_1:def 5;
x in the carrier of M_3 by A104,FUNCT_2:def 1;
then reconsider x as Element of M_3;
(x = z or x = j or x = dj or x = td or x = t) by A1,ENUMSET1:23;
then y=a or y=d or y=c or y=b or y=e by A99,A104;
hence thesis by ENUMSET1:24;
end;
thus ck c= rng f
proof
let y be set;
assume
A105: y in ck;
per cases by A105,ENUMSET1:23;
suppose
A106: y=a;
z in dom f & a = f.z by A99,A102;
hence y in rng f by A106,FUNCT_1:def 5;
suppose
A107: y=b;
j in dom f & b=f.j by A99,A102;
hence y in rng f by A107,FUNCT_1:def 5;
suppose
A108: y=c;
dj in dom f & c = f.dj by A99,A102;
hence y in rng f by A108,FUNCT_1:def 5;
suppose
A109: y=d;
td in dom f & d=f.td by A99,A102;
hence y in rng f by A109,FUNCT_1:def 5;
suppose
A110: y=e;
t in dom f & e=f.t by A99,A102;
hence y in rng f by A110,FUNCT_1:def 5;
end;
end;
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;
A111: {0, 1, 2\1, 3 \ 2, 3} is non empty by ENUMSET1:24;
thus x <= y implies f.x <= f.y
proof
assume
A112: x <= y;
per cases by A1,ENUMSET1:23;
suppose x=z & y=z;hence thesis;
suppose x=z & y=j;
then A113: f.x = a & f.y = b by A99;
a in the carrier of K & b in the carrier of K by A65,ENUMSET1:24;
then reconsider A=a,B=b as Element of K;
a <= b & A in the carrier of K & B in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A113,YELLOW_0:61;
suppose x=z & y=dj;
then A114: f.x = a & f.y = c by A99;
a in the carrier of K & c in the carrier of K by A65,ENUMSET1:24;
then reconsider A=a,C=c as Element of K;
a <= c & A in the carrier of K & C in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A114,YELLOW_0:61;
suppose x=z & y=td;
then A115: f.x = a & f.y = d by A99;
a in the carrier of K & d in the carrier of K by A65,ENUMSET1:24;
then reconsider A=a,D=d as Element of K;
a <= d & A in the carrier of K & D in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A115,YELLOW_0:61;
suppose x=z & y=t;
then A116: f.x = a & f.y = e by A99;
a in the carrier of K & e in the carrier of K by A65,ENUMSET1:24;
then reconsider A=a,E=e as Element of K;
a <= c & c <= e by A64,YELLOW_0:25;
then a <= e & A in the carrier of K & E in the carrier of K
by ORDERS_1:26;
hence f.x <= f.y by A116,YELLOW_0:61;
suppose x=j & y=z;
then j c= z by A111,A112,Def2,YELLOW_1:3;
hence thesis by XBOOLE_1:3;
suppose x=j & y=j;hence thesis;
suppose
A117: x=j & y=dj;
0 in j & not 0 in dj by Th2,CARD_5:1,TARSKI:def 1;
then not j c= dj;
hence thesis by A111,A112,A117,Def2,YELLOW_1:3;
suppose
A118: x=j & y=td;
0 in j & not 0 in td by Th4,CARD_5:1,TARSKI:def 1;
then not j c= td;
hence thesis by A111,A112,A118,Def2,YELLOW_1:3;
suppose x=j & y=t;
then A119: f.x = b & f.y = e by A99;
b in the carrier of K & e in the carrier of K by A65,ENUMSET1:24;
then reconsider B=b,E=e as Element of K;
b <= e & B in the carrier of K & E in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A119,YELLOW_0:61;
suppose x=dj & y=z;
then dj c= z by A111,A112,Def2,YELLOW_1:3;
hence thesis by Th2,XBOOLE_1:3;
suppose
A120: x=dj & y=j;
1 in dj & not 1 in j by Th2,TARSKI:def 1;
then not dj c= j;
hence thesis by A111,A112,A120,Def2,YELLOW_1:3;
suppose x=dj & y=dj;hence thesis;
suppose
A121: x=dj & y=td;
1 in dj & not 1 in td by Th2,Th4,TARSKI:def 1;
then not dj c= td;
hence thesis by A111,A112,A121,Def2,YELLOW_1:3;
suppose x=dj & y=t;
then A122: f.x = c & f.y = e by A99;
c in the carrier of K & e in the carrier of K by A65,ENUMSET1:24;
then reconsider C=c,E=e as Element of K;
c <= e & C in the carrier of K & E in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A122,YELLOW_0:61;
suppose x=td & y=z;
then td c= z by A111,A112,Def2,YELLOW_1:3;
hence thesis by Th4,XBOOLE_1:3;
suppose
A123: x=td & y=j;
2 in td & not 2 in j by Th4,CARD_5:1,TARSKI:def 1;
then not td c= j;
hence thesis by A111,A112,A123,Def2,YELLOW_1:3;
suppose
A124: x=td & y=dj;
2 in td & not 2 in dj by Th2,Th4,TARSKI:def 1;
then not td c= dj;
hence thesis by A111,A112,A124,Def2,YELLOW_1:3;
suppose x=td & y=td;hence thesis;
suppose x=td & y=t;
then A125: f.x = d & f.y = e by A99;
d in the carrier of K & e in the carrier of K by A65,ENUMSET1:24;
then reconsider D=d,E=e as Element of K;
d <= e & D in the carrier of K & E in the carrier of K
by A64,YELLOW_0:25;
hence f.x <= f.y by A125,YELLOW_0:61;
suppose x=t & y=z;
then t c= z by A111,A112,Def2,YELLOW_1:3;
hence thesis by XBOOLE_1:3;
suppose
A126: x=t & y=j;
1 in t & not 1 in j by Th1,ENUMSET1:14;
then not t c= j;
hence thesis by A111,A112,A126,Def2,YELLOW_1:3;
suppose
A127: x=t & y=dj;
2 in t & not 2 in dj by Th1,Th2,ENUMSET1:14,TARSKI:def 1;
then not t c= dj;
hence thesis by A111,A112,A127,Def2,YELLOW_1:3;
suppose
A128: x=t & y=td;
0 in t & not 0 in td by Th1,Th4,ENUMSET1:14,TARSKI:def 1;
then not t c= td;
hence thesis by A111,A112,A128,Def2,YELLOW_1:3;
suppose x=t & y=t;hence thesis;
end;
thus f.x <= f.y implies x <= y
proof
assume
A129: f.x <= f.y;
A130: f.x in ck & f.y in ck by A102,A103,FUNCT_1:def 5;
A131: dj c= t
proof
let X be set;assume X in dj; then X=1 by Th2,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
A132: td c= t
proof
let X be set;assume X in td; then X=2 by Th4,TARSKI:def 1;
hence thesis by Th1,ENUMSET1:14;
end;
per cases by A130,ENUMSET1:23;
suppose f.x = a & f.y = a;
hence x <= y by A100,WAYBEL_1:def 1;
suppose A133: f.x = a & f.y = b;
f.z = a & f.j = b by A99;
then z=x & j = y by A100,A133,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A111,Def2,YELLOW_1:3;
suppose A134: f.x = a & f.y = c;
f.z = a & f.dj = c by A99;
then z=x & dj = y by A100,A134,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A111,Def2,YELLOW_1:3;
suppose A135: f.x = a & f.y = d;
f.z = a & f.td = d by A99;
then z=x & td = y by A100,A135,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A111,Def2,YELLOW_1:3;
suppose A136: f.x = a & f.y = e;
f.z = a & f.t = e by A99;
then z=x & t = y by A100,A136,WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by A111,Def2,YELLOW_1:3;
suppose f.x = b & f.y = a;
then b <= a by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = b & f.y = b;
hence x <= y by A100,WAYBEL_1:def 1;
suppose f.x = b & f.y = c;
then b <= c by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = b & f.y = d;
then b <= d by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose A137: f.x = b & f.y = e;
f.j = b & f.t = e by A99;
then j=x & t = y by A100,A137,WAYBEL_1:def 1;
then x c= y by CARD_1:56;
hence x <= y by A111,Def2,YELLOW_1:3;
suppose f.x = c & f.y = a;
then c <= a by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = c & f.y = b;
then c <= b by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = c & f.y = c;
hence x <= y by A100,WAYBEL_1:def 1;
suppose f.x = c & f.y = d;
then c <= d by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose A138: f.x = c & f.y = e;
f.dj = c & f.t = e by A99;
then dj = x & t = y by A100,A138,WAYBEL_1:def 1;
hence x <= y by A111,A131,Def2,YELLOW_1:3;
suppose f.x = d & f.y = a;
then d <= a & a <= b by A64,A129,YELLOW_0:25,60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = d & f.y = b;
then d <= b by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = d & f.y = c;
then d <= c by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = d & f.y = d;
hence x <= y by A100,WAYBEL_1:def 1;
suppose A139: f.x = d & f.y = e;
f.td = d & f.t = e by A99;
then td=x & t = y by A100,A139,WAYBEL_1:def 1;
hence x <= y by A111,A132,Def2,YELLOW_1:3;
suppose f.x = e & f.y = a;
then e <= a & a <= b by A64,A129,YELLOW_0:25,60;
then e <= b by ORDERS_1:26;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = e & f.y = b;
then e <= b by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = e & f.y = c;
then e <= c by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = e & f.y = d;
then e <= d by A129,YELLOW_0:60;
hence x <= y by A64,YELLOW_0:25;
suppose f.x = e & f.y = e;
hence x <= y by A100,WAYBEL_1:def 1;
end;
end;
hence f is isomorphic by A65,A100,A103,WAYBEL_0:66;
end;
end;
end;
begin:: Modular lattices
definition
let L be non empty RelStr;
attr L is modular means :Def3:
for a,b,c being Element of L st a <= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c;
end;
definition
cluster distributive -> modular
(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,WAYBEL_1:def 3;
end;
hence L is modular by Def3;
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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;
thus
L is modular implies
not ex a,b,c,d,e being Element of L st
(a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
now
given a,b,c,d,e being Element of L such that
A1: a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e and
A2: 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;
A3: b"\/"(c"/\"d) = b by A2,Th5;
b <= d by A2,YELLOW_0:23;
hence not L is modular by A1,A2,A3,Def3;
end;
hence thesis;
end;
now
assume
not L is modular;
then consider x,y,z being Element of L such that
A4: x <= z & x"\/"(y"/\"z) <> (x"\/"y)"/\"z by Def3;
A5: x"\/"(y"/\"z) <> (x"\/"y)"/\"z & x"\/"(y"/\"z) <= (x"\/"y)"/\"z by A4,Th8;
set b=y"/\"z;
set x1=x"\/"(y"/\"z);
set y1=y;
set z1=(x"\/"y)"/\"z;
set t=x"\/"y;
y"/\"z <= x1 & y"/\"z <= y1 by YELLOW_0:22,23;
then (y"/\"z)"/\"(y"/\"z) <= x1"/\"y1 by YELLOW_3:2;
then A6: y"/\"z <= x1"/\"y1 by YELLOW_5:2;
x"\/"(y"/\"z) <= z"\/"(y"/\"z) by A4,YELLOW_5:7;
then x"\/"(y"/\"z) <= z & y <= y by LATTICE3:17;
then A7: x1"/\"y1 <= y"/\"z by YELLOW_3:2;
A8: b <> t
proof
now
assume
A9: b=t;
then (x"\/"y)"/\"z = y"/\"(z"/\"z) by LATTICE3:16
.= x"\/"y by A9,YELLOW_5:2
.= (x"\/"x)"\/"y by YELLOW_5:1
.= x"\/"(y"/\"z) by A9,LATTICE3:14;
hence contradiction by A4;
end;
hence thesis;
end;
A10: z1 <= x"\/"y & y1 <= x"\/"y by YELLOW_0:22,23;
x <= z & (x"\/"y) <= (x"\/"y) by A4;
then (x"\/"y)"/\"x <= (x"\/"y)"/\"z by YELLOW_3:2;
then x <= (x"\/"y)"/\"z by LATTICE3:18;
then A11: x"\/"y <= z1"\/"y1 by YELLOW_5:7;
thus
ex a,b,c,d,e being Element of L st
a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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 b,x1,y1,z1,t as Element of L;
take b,x1,y1,z1,t;
thus b<>x1
proof
now
assume
A12: b=x1;
then x <= y"/\"z & y"/\"z <= y by YELLOW_0:22,23;
then x <= y by YELLOW_0:def 2;
hence contradiction by A4,A12,YELLOW_5:8;
end;
hence thesis;
end;
thus b<>y1
proof
now
assume
A13: b=y1;
then x <= z & y <= z by A4,YELLOW_0:23;
then x"\/"y <= z by YELLOW_5:9;
hence contradiction by A4,A13,YELLOW_5:10;
end;
hence thesis;
end;
thus b<>z1
proof
now
assume
b=z1;
then A14: (x"\/"y)"/\"z <= x"\/"(y"/\"z) by YELLOW_0:22;
x"\/"(y"/\"z) <= (x"\/"y)"/\"z by A4,Th8;
hence contradiction by A4,A14,YELLOW_0:def 3;
end;
hence thesis;
end;
thus b<>t by A8;
thus x1<>y1
proof
now
assume
x1=y1;
then A15: x1"/\"y1 = x1 & x1"\/"y1 = x1 by YELLOW_5:1,2;
x1"\/"y1 = x "\/" ((y"/\"z)"\/"y) by LATTICE3:14
.= t by LATTICE3:17;
hence contradiction by A6,A7,A8,A15,YELLOW_0:def 3;
end;
hence thesis;
end;
thus x1<>z1 by A4;
thus x1<>t
proof
now
assume t=x1;
then A16: (x"\/"y)"/\"z <= x"\/"(y"/\"z) by YELLOW_0:23;
x"\/"(y"/\"z) <= (x"\/"y)"/\"z by A4,Th8;
hence contradiction by A4,A16,YELLOW_0:def 3;
end;
hence thesis;
end;
thus y1<>z1
proof
now
assume
y1=z1;
then A17: z1"/\"y1 = z1 & z1"\/"y1 = z1 by YELLOW_5:1,2;
y1"/\"z1 = ((x"\/"y)"/\"y)"/\"z by LATTICE3:16
.= b by LATTICE3:18;
hence contradiction by A8,A10,A11,A17,YELLOW_0:def 3;
end;
hence thesis;
end;
thus y1<>t
proof
now
assume
A18: y1=t;
then x <= z & x <= y by A4,YELLOW_0:22;
then x "/\" x <= y"/\"z by YELLOW_3:2;
then x <= y"/\"z by YELLOW_5:2;
hence contradiction by A4,A18,YELLOW_5:8;
end;
hence thesis;
end;
thus z1<>t
proof
now
assume
A19: z1=t;
then y <= x"\/"y & x"\/"y <= z by YELLOW_0:22,23;
then y <= z by YELLOW_0:def 2;
hence contradiction by A4,A19,YELLOW_5:10;
end;
hence thesis;
end;
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 A6,A7,YELLOW_0:def 3;
thus x1"/\"z1 = x1 by A5,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;
z1 <= x"\/"y & y1 <= x"\/"y by YELLOW_0:22,23;
then A20: y1"\/"z1 <= x"\/"y by YELLOW_5:9;
x <= z & (x"\/"y) <= (x"\/"y) by A4;
then (x"\/"y)"/\"x <= (x"\/"y)"/\"z by YELLOW_3:2;
then x <= (x"\/"y)"/\"z by LATTICE3:18;
then x"\/"y <= z1"\/"y1 by YELLOW_5:7;
hence y1"\/"z1 = t by A20,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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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;
thus L is distributive implies
not ex a,b,c,d,e being Element of L st
a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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
now
given a,b,c,d,e being Element of L such that
A2: a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e
and
A3: 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;
(b"/\"c)"\/"(b"/\"d) = a by A3,YELLOW_5:1;
hence not L is distributive by A2,A3,WAYBEL_1:def 3;
end;
hence thesis;
end;
now
assume
not L is distributive;
then consider x,y,z being Element of L such that
A4: x"/\"(y"\/"z) <> (x"/\"y)"\/"(x"/\"z) by WAYBEL_1:def 3;
set b=(x"/\"y)"\/"(y"/\"z)"\/"(z"/\"x);
set t=(x"\/"y)"/\"(y"\/"z)"/\"(z"\/"x);
A5: b <= t
proof
A6: (x"/\"y) <= (x"\/"y) & (x"/\"y) <= (y"\/"z) & (x"/\"y) <= (z"\/"
x) by YELLOW_5:5;
A7: (y"/\"z) <= (x"\/"y) & (y"/\"z) <= (y"\/"z) & (y"/\"z) <= (z"\/"
x) by YELLOW_5:5;
A8: (z"/\"x) <= (x"\/"y) & (z"/\"x) <= (y"\/"z) & (z"/\"x) <= (z"\/"
x) by YELLOW_5:5;
(x"/\"y) "/\" (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) by A6,YELLOW_3:2;
then (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2;
then (x"/\"y) "/\" (x"/\"y) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/"
x) by A6,YELLOW_3:2;
then A9: (x"/\"y) <= t by YELLOW_5:2;
(y"/\"z) "/\" (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) by A7,YELLOW_3:2;
then (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2;
then (y"/\"z) "/\" (y"/\"z) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/"
x) by A7,YELLOW_3:2;
then A10: (y"/\"z) <= t by YELLOW_5:2;
(z"/\"x) "/\" (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) by A8,YELLOW_3:2;
then (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) by YELLOW_5:2;
then (z"/\"x) "/\" (z"/\"x) <= (x"\/"y) "/\" (y"\/"z) "/\" (z"\/"
x) by A8,YELLOW_3:2;
then A11: (z"/\"x) <= t by YELLOW_5:2;
(x"/\"y)"\/"(y"/\"z) <= t"\/"t by A9,A10,YELLOW_3:3;
then (x"/\"y)"\/"(y"/\"z) <= t by YELLOW_5:1;
then (x"/\"y)"\/"(y"/\"z)"\/"(z"/\"x) <= t"\/"t by A11,YELLOW_3:3;
hence thesis by YELLOW_5:1;
end;
A12: z"/\"x <= x & x"/\"y <= x by YELLOW_0:23;
(y"/\"z) <= z & x <= x by YELLOW_0:23;
then (y"/\"z)"/\"x <= z"/\"x by YELLOW_3:2;
then A13: ((y"/\"z)"/\"x) "\/" (z"/\"x) = z"/\"x by YELLOW_5:8;
A14: 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;
A15: b <> t
proof
now
assume b=t;
then x"/\"(y"\/"z) = ((x"/\"y)"\/"((y"/\"z)"\/"(z"/\"x)))"/\"
x by A14,LATTICE3:14
.= (x"/\"y)"\/"(((y"/\"z)"\/"(z"/\"x))"/\"x) by A1,A12,Def3
.= (x"/\"y)"\/"(z"/\"x) by A1,A12,A13,Def3;
hence contradiction by A4;
end;
hence thesis;
end;
set x1=(x"\/"b)"/\"t;
set y1=(y"\/"b)"/\"t;
set z1=(z"\/"b)"/\"t;
A16: 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;
A17: 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;
A18: 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;
A19: 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;
A20: 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;
A21: 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;
A22: b <= (x"/\"t)"\/"(y"/\"t)
proof
(x"/\"y)"\/"(x"/\"z) <= x"/\"(y"\/"z) & (x"/\"y)"\/"(y"/\"z) <= y"/\"(
x
"\/"z) by Th6;
then ((x"/\"y)"\/"(x"/\"z))"\/"((x"/\"y)"\/"(y"/\"z)) <= (x"/\"(y"\/"z)
) "\/"
(y"/\"(x"\/"z))
by 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;
hence thesis by A16,A17,LATTICE3:14;
end;
A23: b <= (x"/\"t)"\/"(z"/\"t)
proof
(x"/\"z)"\/"(x"/\"y) <= x"/\"(z"\/"y) & (x"/\"z)"\/"(z"/\"y) <= z"/\"(
x
"\/"y) by Th6;
then ((x"/\"z)"\/"(x"/\"y))"\/"((x"/\"z)"\/"(z"/\"y)) <= (x"/\"(z"\/"y)
) "\/"
(z"/\"(x"\/"y))
by 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;
hence thesis by A16,A18,LATTICE3:14;
end;
A24: b <= (z"/\"t)"\/"(y"/\"t)
proof
(z"/\"y)"\/"(z"/\"x) <= z"/\"(y"\/"x) & (z"/\"y)"\/"(y"/\"x) <= y"/\"(
z
"\/"x) by Th6;
then ((z"/\"y)"\/"(z"/\"x))"\/"((z"/\"y)"\/"(y"/\"x)) <= (z"/\"(y"\/"x)
) "\/"
(y"/\"(z"\/"x))
by 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;
hence thesis by A17,A18,LATTICE3:14;
end;
A25: (x"\/"b)"/\"(y"\/"b) <= t
proof
x"\/"(y"/\"z) <= (x"\/"y)"/\"(x"\/"z) & y"\/"(x"/\"z) <= (y"\/"x)"/\"(
y
"\/"z) by Th7;
then (x"\/"(y"/\"z))"/\"(y"\/"(x"/\"z)) <= ((x"\/"y)"/\"(x"\/"z))"/\"((
y"\/"
x)"/\"(y"\/"z))
by YELLOW_3:2;
then (x"\/"b)"/\"(y"\/"b) <=
((x"\/"z)"/\"(x"\/"y))"/\"(x"\/"y)"/\"(y"\/"z) by A19,A20,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;
hence thesis by LATTICE3:16;
end;
A26: (x"\/"b)"/\"(z"\/"b) <= t
proof
x"\/"(z"/\"y) <= (x"\/"z)"/\"(x"\/"y) & z"\/"(x"/\"y) <= (z"\/"x)"/\"(
z
"\/"y) by Th7;
then (x"\/"(z"/\"y))"/\"(z"\/"(x"/\"y)) <= ((x"\/"z)"/\"(x"\/"y))"/\"((
z"\/"
x)"/\"(z"\/"y))
by YELLOW_3:2;
then (x"\/"b)"/\"(z"\/"b) <=
((x"\/"y)"/\"(x"\/"z))"/\"(x"\/"z)"/\"(z"\/"y) by A19,A21,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;
hence thesis by LATTICE3:16;
end;
A27: (z"\/"b)"/\"(y"\/"b) <= t
proof
z"\/"(y"/\"x) <= (z"\/"y)"/\"(z"\/"x) & y"\/"(z"/\"x) <= (y"\/"z)"/\"(
y
"\/"x) by Th7;
then (z"\/"(y"/\"x))"/\"(y"\/"(z"/\"x)) <= ((z"\/"y)"/\"(z"\/"x))"/\"((
y"\/"
z)"/\"(y"\/"x))
by YELLOW_3:2;
then (z"\/"b)"/\"(y"\/"b) <=
((z"\/"x)"/\"(z"\/"y))"/\"(z"\/"y)"/\"(y"\/"x) by A20,A21,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;
hence thesis by LATTICE3:16;
end;
x"/\"(y"\/"z) <= x & x <= x"\/"z by YELLOW_0:22,23;
then A28: x"/\"(y"\/"z) <= x"\/"z by YELLOW_0:def 2;
x"/\"(z"\/"y) <= x & x <= x"\/"y by YELLOW_0:22,23;
then A29: x"/\"(z"\/"y) <= x"\/"y by YELLOW_0:def 2;
z"/\"(y"\/"x) <= z & z <= z"\/"x by YELLOW_0:22,23;
then A30: z"/\"(y"\/"x) <= z"\/"x by YELLOW_0:def 2;
x"/\"z <= x & x <= x"\/"(y"/\"z) by YELLOW_0:22,23;
then A31: x"/\"z <= x"\/"(y"/\"z) by YELLOW_0:def 2;
x"/\"y <= x & x <= x"\/"(z"/\"y) by YELLOW_0:22,23;
then A32: x"/\"y <= x"\/"(z"/\"y) by YELLOW_0:def 2;
z"/\"x <= z & z <= z"\/"(y"/\"x) by YELLOW_0:22,23;
then A33: z"/\"x <= z"\/"(y"/\"x) by YELLOW_0:def 2;
A34: y <= y"\/"z by YELLOW_0:22;
A35: z <= z"\/"y by YELLOW_0:22;
A36: y <= y"\/"x by YELLOW_0:22;
A37: y"/\"z <= y by YELLOW_0:23;
A38: z"/\"y <= z by YELLOW_0:23;
A39: y"/\"x <= y by YELLOW_0:23;
A40: y1 = (y"/\"t)"\/"b by A1,A5,Def3;
A41: z1 = (z"/\"t)"\/"b by A1,A5,Def3;
A42: x1 "\/" y1 = ((x"/\"t)"\/"b) "\/" ((y"/\"t)"\/"b) by A1,A5,A40,Def3
.= (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 A16,A17,A22,YELLOW_5:8
.= (y"\/"(x "/\"(y"\/"z))) "/\"(x"\/"z) by A1,A28,Def3
.= t by A1,A34,Def3;
A43: 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 A19,A20,A25,YELLOW_5:10
.= (y"/\"(x "\/"(y"/\"z))) "\/"(x"/\"z) by A1,A31,Def3
.= b by A1,A37,Def3;
A44: x1 "\/" z1 = ((x"/\"t)"\/"b) "\/" ((z"/\"t)"\/"b) by A1,A5,A41,Def3
.= (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 A16,A18,A23,YELLOW_5:8
.= (z"\/"(x "/\"(z"\/"y))) "/\"(x"\/"y) by A1,A29,Def3
.= (z"\/"x)"/\"(z"\/"y)"/\"(x"\/"y) by A1,A35,Def3
.= t by LATTICE3:16;
A45: 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 A19,A21,A26,YELLOW_5:10
.= (z"/\"(x "\/"(z"/\"y))) "\/"(x"/\"y) by A1,A32,Def3
.= (z"/\"x)"\/"(z"/\"y)"\/"(x"/\"y) by A1,A38,Def3
.= b by LATTICE3:14;
A46: z1 "\/" y1 = ((z"/\"t)"\/"b) "\/" ((y"/\"t)"\/"b) by A1,A5,A40,Def3
.= (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 A17,A18,A24,YELLOW_5:8
.= (y"\/"(z "/\"(y"\/"x))) "/\"(z"\/"x) by A1,A30,Def3
.= t by A1,A36,Def3;
A47: 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 A20,A21,A27,YELLOW_5:10
.= (y"/\"(z "\/"(y"/\"x))) "\/"(z"/\"x) by A1,A33,Def3
.= b by A1,A39,Def3;
b <= x1 by A43,YELLOW_0:23;
then A48: b "\/" x1 = x1 by YELLOW_5:8;
b <= y1 by A43,YELLOW_0:23;
then A49: b "\/" y1 = y1 by YELLOW_5:8;
b <= z1 by A45,YELLOW_0:23;
then A50: b "\/" z1 = z1 by YELLOW_5:8;
x1 <= t by YELLOW_0:23;
then A51: t "/\" x1 = x1 by YELLOW_5:10;
y1 <= t by YELLOW_0:23;
then A52: t "/\" y1 = y1 by YELLOW_5:10;
z1 <= t by YELLOW_0:23;
then A53: t "/\" z1 = z1 by YELLOW_5:10;
thus
ex a,b,c,d,e being Element of L st
a<>b & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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 b,x1,y1,z1,t as Element of L;
take b,x1,y1,z1,t;
thus b<>x1 by A15,A42,A44,A47,A49,A50,YELLOW_5:2;
thus b<>y1 by A15,A42,A45,A46,A48,A50,YELLOW_5:2;
thus b<>z1 by A15,A43,A44,A46,A48,A49,YELLOW_5:2;
thus b<>t by A15;
thus x1<>y1
proof
now
assume x1=y1;
then x1"/\"y1=x1 & x1"\/"y1=x1 by YELLOW_5:1,2;
hence contradiction by A15,A42,A43;
end;
hence thesis;
end;
thus x1<>z1
proof
now
assume x1=z1;
then x1"/\"z1=x1 & x1"\/"z1=x1 by YELLOW_5:1,2;
hence contradiction by A15,A44,A45;
end;
hence thesis;
end;
thus x1<>t by A15,A43,A45,A46,A52,A53,YELLOW_5:1;
thus y1<>z1
proof
now
assume y1=z1;
then y1"/\"z1=y1 & y1"\/"z1=y1 by YELLOW_5:1,2;
hence contradiction by A15,A46,A47;
end;
hence thesis;
end;
thus y1<>t by A15,A43,A44,A47,A51,A53,YELLOW_5:1;
thus z1<>t by A15,A42,A45,A47,A51,A52,YELLOW_5:1;
thus b"/\"x1 = b
proof
b <= x1 by A43,YELLOW_0:23;
hence thesis by YELLOW_5:10;
end;
thus b"/\"y1 = b
proof
b <= y1 by A43,YELLOW_0:23;
hence thesis by YELLOW_5:10;
end;
thus b"/\"z1 = b
proof
b <= z1 by A45,YELLOW_0:23;
hence thesis by YELLOW_5:10;
end;
thus x1"/\"t = x1
proof
x1 <= t by A42,YELLOW_0:22;
hence thesis by YELLOW_5:10;
end;
thus y1"/\"t = y1
proof
y1 <= t by A42,YELLOW_0:22;
hence thesis by YELLOW_5:10;
end;
thus z1"/\"t = z1
proof
z1 <= t by A44,YELLOW_0:22;
hence thesis by YELLOW_5:10;
end;
thus x1"/\"y1 = b by A43;
thus x1"/\"z1 = b by A45;
thus y1"/\"z1 = b by A47;
thus x1"\/"y1 = t by A42;
thus x1"\/"z1 = t by A44;
thus y1"\/"z1 = t by A46;
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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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 A1,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 & a<>c & a<>d & a<>e & b<>c & b<>d & b<>e & c <>d & c <>e & d<>e &
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[set] means
ex c1 being Element of L st c1=$1 & a <= c1 & c1 <= b;
consider S being set such that
A1: for c being set holds c in S iff c in the carrier of L & P[c]
from Separation;
for c being set 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 consider c1 being Element of L such that
A2: c1=c & a <= c1 & c1 <= b by A1;
thus thesis by A2;
end;
thus a <= c & c <= b implies c in S by A1;
end;
end;
uniqueness
proof
let x,y be Subset of L;
assume that
A3: for c being Element of L holds c in x iff a <= c & c <= b and
A4: for c being Element of L holds c in y iff a <= c & c <= b;
A5: now
let c1 be set;
assume
A6: c1 in x;
then reconsider c = c1 as Element of L;
c in x iff a <= c & c <= b by A3;
hence c1 in y by A4,A6;
end;
now
let c1 be set;
assume
A7: c1 in y;
then reconsider c = c1 as Element of L;
c in y iff a <= c & c <= b by A4;
hence c1 in x by A3,A7;
end;
then x c= y & y c= x by A5,TARSKI:def 3;
hence x=y by XBOOLE_0:def 10;
end;
end;
definition
let L be non empty RelStr;
let IT be Subset of L;
attr IT is interval means :Def5:
ex a,b being Element of L st IT = [#a,b#];
end;
definition
let L be non empty reflexive transitive RelStr;
cluster non empty interval -> directed (Subset of L);
coherence
proof
let M be Subset of L;
assume
A1: M is non empty interval;
then consider a,b being Element of L such that
A2: M = [#a,b#] by Def5;
let x,y be Element of L;
assume
A3: x in M & y in M;
take b;
consider z being set such that
A4: z in M by A1,XBOOLE_0:def 1;
reconsider z as Element of L by A4;
a <= z & z <= b by A2,A4,Def4;
then a <= b & b <= b by ORDERS_1:26;
hence b in M by A2,Def4;
thus x <= b & y <= b by A2,A3,Def4;
end;
cluster non empty interval -> filtered (Subset of L);
coherence
proof
let M be Subset of L;
assume
A5: M is non empty interval;
then consider a,b being Element of L such that
A6: M = [#a,b#] by Def5;
let x,y be Element of L;
assume
A7: x in M & y in M;
take a;
consider z being set such that
A8: z in M by A5,XBOOLE_0:def 1;
reconsider z as Element of L by A8;
a <= z & z <= b by A6,A8,Def4;
then a <= a & a <= b by ORDERS_1:26;
hence a in M by A6,Def4;
thus a <= x & a <= y by A6,A7,Def4;
end;
end;
definition
let L be non empty RelStr;
let a,b be Element of L;
cluster [#a,b#] -> interval;
coherence by Def5;
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 set; assume
A1: x in [#a,b#];
then reconsider y=x as Element of L;
A2: a <= y & y <= b by A1,Def4;
a in {a} & b in {b} by TARSKI:def 1;
then y in {z where z is Element of L :
ex w being Element of L st z >= w & w in {a}} &
y in {z where z is Element of L :
ex w being Element of L st z <= w & w in {b}} by A2;
then y in uparrow {a} & y in downarrow {b} by WAYBEL_0:14,15;
then y in (uparrow {a}) /\ (downarrow {b}) by XBOOLE_0:def 3;
then y in (uparrow a) /\ (downarrow {b}) by WAYBEL_0:def 18;
hence x in uparrow a /\ downarrow b by WAYBEL_0:def 17;
end;
thus uparrow a /\ downarrow b c= [#a,b#]
proof
let x be set;
assume x in uparrow a /\ downarrow b;
then x in (uparrow a) /\ (downarrow {b}) by WAYBEL_0:def 17;
then x in (uparrow {a}) /\ (downarrow {b}) by WAYBEL_0:def 18;
then x in uparrow {a} & x in downarrow {b} by XBOOLE_0:def 3;
then A3: x in {z where z is Element of L :
ex w being Element of L st z >= w & w in {a}} &
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,15;
then consider y1 being Element of L such that
A4: x=y1 & ex w being Element of L st y1 >= w & w in {a};
ex y2 being Element of L st x=y2 & ex w being Element of L st
y2 <= w & w in {b} by A3;
then a <= y1 & y1 <= b by A4,TARSKI:def 1;
hence thesis by A4,Def4;
end;
end;
definition
let L be with_infima Poset;
let a,b be Element of L;
cluster subrelstr[#a,b#] -> meet-inheriting;
coherence
proof
set ab = subrelstr[#a,b#];
let x,y be Element of L;
assume
x in the carrier of ab & y in the carrier of ab & ex_inf_of {x,y},L;
then x in [#a,b#] & y in [#a,b#] by YELLOW_0:def 15;
then A1: x <= b & a <= x & a <= y by Def4;
A2: inf {x,y} = x"/\"y by YELLOW_0:40;
then inf {x,y} <= x & inf {x,y} <= y by YELLOW_0:23;
then A3: inf {x,y} <= b by A1,YELLOW_0:def 2;
a <= inf {x,y} by A1,A2,YELLOW_0:23;
then inf {x,y} in [#a,b#] by A3,Def4;
hence inf {x,y} in the carrier of ab by YELLOW_0:def 15;
end;
end;
definition
let L be with_suprema Poset;
let a,b be Element of L;
cluster subrelstr[#a,b#] -> join-inheriting;
coherence
proof
set ab = subrelstr([#a,b#]);
let x,y be Element of L; assume
x in the carrier of ab & y in the carrier of ab & ex_sup_of {x,y},L;
then x in [#a,b#] & y in [#a,b#] by YELLOW_0:def 15;
then A1: x <= b & y <= b & a <= x & a <= y by Def4;
A2: sup {x,y} = x"\/"y by YELLOW_0:41;
then x <= sup {x,y} & y <= sup {x,y} by YELLOW_0:22;
then A3: a <= sup {x,y} by A1,YELLOW_0:def 2;
sup {x,y} <= b by A1,A2,YELLOW_0:22;
then sup {x,y} in [#a,b#] by A3,Def4;
hence sup {x,y} in the carrier of ab 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[set,set] 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 set st x in the carrier of subrelstr[#b,a"\/"b#]
ex y being set st y in the carrier of subrelstr[#a"/\"b,a#] & P[x,y]
proof
let x be set;
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;
b <= x1 & x1 <= a"\/"b by A3,Def4;
then a"/\"b <= y & y <= a"/\"(a"\/"b) by YELLOW_5:6;
then a"/\"b <= y & y <= a by LATTICE3:18;
then y in [#(a"/\"b),a#] by 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
A4: for x being set st x in the carrier of subrelstr[#b,a"\/"b#]
holds P[x,f.x] from FuncEx1(A2);
reconsider f as map of subrelstr[#b,a"\/"b#],subrelstr[#(a"/\"b),a#];
take f;
thus f is isomorphic
proof
subrelstr([#b,b"\/"a#]) is non empty
proof
b <= b & b <= a"\/"b by YELLOW_0:22;
then b in [#b,a"\/"b#] by Def4;
then b in the carrier of subrelstr([#b,a"\/"b#]) by YELLOW_0:def 15;
hence thesis by STRUCT_0:def 1;
end;
then reconsider s1 = subrelstr([#b,b"\/"
a#]) as non empty full Sublattice of L;
subrelstr([#(a"/\"b),a#]) is non empty
proof
a"/\"b <= a"/\"b & a"/\"b <= a by YELLOW_0:23;
then a"/\"b in [#a"/\"b,a#] by Def4;
then a"/\"b in the carrier of subrelstr([#a"/\"b,a#]) by YELLOW_0:def
15;
hence thesis by STRUCT_0:def 1;
end;
then reconsider s2 = subrelstr[#(a"/\"
b),a#] as non empty full Sublattice of L;
reconsider f1 = f as map of s1,s2;
A5: dom f1 = the carrier of subrelstr[#b,a"\/"b#] by FUNCT_2:def 1;
then A6: dom f1 = [#b,a"\/"b#] by YELLOW_0:def 15;
A7: f1 is one-to-one
proof
let x1,x2 be set;
assume
A8: x1 in dom f1 & x2 in dom f1 & f1.x1 = f1.x2;
then reconsider X1 = x1 as Element of L by A6;
reconsider X2 = x2 as Element of L by A6,A8;
reconsider f1X1 = f1.X1 as Element of L by A4,A5,A8;
reconsider f1X2 = f1.X2 as Element of L by A4,A5,A8;
A9: b <= X1 & X1 <= a"\/"b & b <= X2 & X2 <= a"\/"b by A6,A8,Def4;
A10: f1X1 = X1 "/\" a & f1X2 = X2 "/\" a by A4,A5,A8;
X1 = (b "\/" a) "/\" X1 by A9,YELLOW_5:10
.= b "\/" (a "/\" X2) by A1,A8,A9,A10,Def3
.= (b "\/" a) "/\" X2 by A1,A9,Def3
.= X2 by A9,YELLOW_5:10;
hence x1 = x2;
end;
A11: rng f1 = the carrier of subrelstr[#(a"/\"b),a#]
proof
thus rng f1 c= the carrier of subrelstr[#(a"/\"b),a#];
thus the carrier of subrelstr[#(a"/\"b),a#] c= rng f1
proof
let y be set;
assume y in the carrier of subrelstr[#(a"/\"b),a#];
then A12: y in [#(a"/\"b),a#] by YELLOW_0:def 15;
then reconsider Y = y as Element of L;
A13: a"/\"b <= Y & Y <= a by A12,Def4;
then (a"/\"b)"\/"b <= Y"\/"b & Y"\/"b <= a"\/"b by WAYBEL_1:3;
then b <= Y"\/"b & Y"\/"b <= a"\/"b by LATTICE3:17;
then A14: Y"\/"b in [#b,a"\/"b#] by Def4;
then A15: 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 A4;
f1yb = (Y"\/"b)"/\"a by A4,A15
.= Y"\/"(b"/\"a) by A1,A13,Def3
.= Y by A13,YELLOW_5:8;
hence y in rng f1 by A6,A14,FUNCT_1:def 5;
end;
end;
for x,y being Element of s1 holds x <= y iff f1.x <= f1.y
proof
let x,y be Element of s1;
A16: the carrier of s1 = [#b,a"\/"b#] by YELLOW_0:def 15;
then A17: x in [#b,a"\/"b#] & y in [#b,a"\/"b#];
then reconsider X = x as Element of L;
reconsider Y = y as Element of L by A17;
reconsider f1X = f1.X as Element of L by A4;
reconsider f1Y = f1.Y as Element of L by A4;
thus x <= y implies f1.x <= f1.y
proof
assume
x <= y;
then A18: [x,y] in the InternalRel of s1 by ORDERS_1:def 9;
the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13;
then A19: X <= Y by A18,ORDERS_1:def 9;
f1X = X"/\"a & f1Y = Y"/\"a by A4;
then f1X <= f1Y by A19,WAYBEL_1:2;
hence thesis by YELLOW_0:61;
end;
thus f1.x <= f1.y implies x <= y
proof
assume f1.x <= f1.y;
then A20: [f1.x,f1.y] in the InternalRel of s2 by ORDERS_1:def
9;
the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13;
then A21: f1X <= f1Y by A20,ORDERS_1:def 9;
f1X = X"/\"a & f1Y = Y"/\"a by A4;
then A22: b"\/"(a"/\"X) <= b"\/"(a"/\"Y) by A21,WAYBEL_1:3;
A23: b <= X & X <= b"\/"a & b <= Y & Y <= b"\/"a by A16,Def4;
then (b"\/"a)"/\"X <= b"\/"(a"/\"Y) by A1,A22,Def3;
then (b"\/"a)"/\"X <= (b"\/"a)"/\"Y by A1,A23,Def3;
then X <= (b"\/"a)"/\"Y by A23,YELLOW_5:10;
then X <= Y by A23,YELLOW_5:10;
hence thesis by YELLOW_0:61;
end;
end;
hence thesis by A7,A11,WAYBEL_0:66;
end;
end;
definition
cluster finite non empty LATTICE;
existence
proof
consider s being set;
set D = {s};
consider R being Order of D;
reconsider A = RelStr (#D,R#) as with_infima with_suprema Poset;
take A;
thus thesis by GROUP_1:def 13;
end;
end;
definition
cluster finite -> lower-bounded Semilattice;
coherence
proof
let L be Semilattice;
defpred P[set] means ex x being Element of L st x is_<=_than $1;
assume L is finite; then
A1: the carrier of L is finite by GROUP_1:def 13;
A2: P[{}]
proof
consider a being Element of L;
take a;
let b be Element of L;
assume b in {};
hence thesis;
end;
A3: 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
A4: x in the carrier of L and
B c= the carrier of L;
given a being Element of L such that
A5: a is_<=_than B;
reconsider y=x as Element of L by A4;
take b = a"/\"y;
let c be Element of L;
assume
A6: c in B \/ {x};
A7: now
assume c in B;
then a <= c & a"/\"y <= a by A5,LATTICE3:def 8,YELLOW_0:23;
hence a"/\"y <= c by ORDERS_1:26;
end;
now
assume c in {x};
then c = y by TARSKI:def 1;
hence b <= c by YELLOW_0:23;
end;
hence thesis by A6,A7,XBOOLE_0:def 2;
end;
thus P[the carrier of L] from Finite(A1,A2,A3);
end;
end;
definition
cluster finite -> complete LATTICE;
coherence
proof
let L be LATTICE;
assume
A1: L is finite;
then A2: the carrier of L is finite by GROUP_1:def 13;
for x being Subset of L holds ex_sup_of x,L
proof
let x be Subset of L;
per cases;
suppose
A3: x = {};
L is finite LATTICE by A1;
hence thesis by A3,YELLOW_0:42;
suppose
A4: x <> {};
x is finite by A2,FINSET_1:13;
hence thesis by A4,YELLOW_0:54;
end;
hence thesis by YELLOW_0:53;
end;
end;