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&qu