set cn = the carrier of N_5;
let L be LATTICE; :: thesis:
A1: the carrier of N_5 = {0,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
thus ( ex K being full Sublattice of L st N_5 ,K are_isomorphic implies ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ) :: thesis:

reconsider td = 3 \ 2 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider dw = 2 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider cl = the carrier of L as non empty set ;
reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;
given K being full Sublattice of L such that A2: N_5 ,K are_isomorphic ; :: thesis:
consider f being Function of N_5,K such that
A3: f is isomorphic by A2;
A4: not K is empty by A3, WAYBEL_0:def 38;
then A5: ( f is one-to-one & f is monotone ) by A3, WAYBEL_0:def 38;
reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;
reconsider ck = the carrier of K as non empty set ;
A6: ck = rng f by A3, WAYBEL_0:66;
reconsider g = f as Function of the carrier of N_5,ck ;
reconsider a = g . z, b = g . td, c = g . dw, d = g . tj, e = g . t as Element of K ;
reconsider ck = ck as non empty Subset of cl by YELLOW_0:def 13;
A7: b in ck ;
A8: c in ck ;
A9: e in ck ;
A10: d in ck ;
a in ck ;
then reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;
take A ; :: thesis:
take B ; :: thesis:
take C ; :: thesis:
take D ; :: thesis:
take E ; :: thesis:
thus A <> B by A5, Th4, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis:
thus A <> C by A5, WAYBEL_1:def 1; :: thesis:
thus A <> D by A5, Th3, WAYBEL_1:def 1; :: thesis:
thus A <> E by A5, WAYBEL_1:def 1; :: thesis:

assume f . td = f . dw ; :: thesis:
then A11: td = dw by A4, A5, WAYBEL_1:def 1;
2 in td by Th4, TARSKI:def 1;
hence contradiction by A11; :: thesis:

end;

hence B <> C ; :: thesis:

now :: thesis:

A12: 1 in tj by Th3, TARSKI:def 2;
assume A13: f . td = f . tj ; :: thesis:
not 1 in td by Th4, TARSKI:def 1;
hence contradiction by A4, A5, A13, A12, WAYBEL_1:def 1; :: thesis:

end;

hence B <> D ; :: thesis:

now :: thesis:

A14: 1 in t by CARD_1:51, ENUMSET1:def 1;
assume A15: f . td = f . t ; :: thesis:
not 1 in td by Th4, TARSKI:def 1;
hence contradiction by A4, A5, A15, A14, WAYBEL_1:def 1; :: thesis:

end;

hence B <> E ; :: thesis:

now :: thesis:

assume f . dw = f . tj ; :: thesis:
then A16: dw = tj by A4, A5, WAYBEL_1:def 1;
2 in tj by Th3, TARSKI:def 2;
hence contradiction by A16; :: thesis:

end;

hence C <> D ; :: thesis:
thus C <> E by A5, WAYBEL_1:def 1; :: thesis:

now :: thesis:

A17: 0 in t by CARD_1:51, ENUMSET1:def 1;
assume A18: f . tj = f . t ; :: thesis:
not 0 in tj by Th3, TARSKI:def 2;
hence contradiction by A4, A5, A18, A17, WAYBEL_1:def 1; :: thesis:

end;

hence D <> E ; :: thesis:
z c= td ;
then z <= td by YELLOW_1:3;
then a <= b by A3, WAYBEL_0:66;
then A <= B by YELLOW_0:59;
hence A "/\" B = A by YELLOW_0:25; :: thesis:
z c= dw ;
then z <= dw by YELLOW_1:3;
then a <= c by A3, WAYBEL_0:66;
then A <= C by YELLOW_0:59;
hence A "/\" C = A by YELLOW_0:25; :: thesis:
Segm 2 c= Segm 3 by NAT_1:39;
then dw <= t by YELLOW_1:3;
then c <= e by A3, WAYBEL_0:66;
then C <= E by YELLOW_0:59;
hence C "/\" E = C by YELLOW_0:25; :: thesis:
tj <= t by YELLOW_1:3;
then d <= e by A3, WAYBEL_0:66;
then D <= E by YELLOW_0:59;
hence D "/\" E = D by YELLOW_0:25; :: thesis:
thus B "/\" C = A :: thesis:

proof

A19: now :: thesis:

assume B "/\" C = D ; :: thesis:
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:60;
then tj <= dw by A3, WAYBEL_0:66;
then A20: tj c= dw by YELLOW_1:3;
2 in tj by Th3, TARSKI:def 2;
then 2 in 2 by A20;
hence contradiction ; :: thesis:

end;

A21: now :: thesis:

assume B "/\" C = E ; :: thesis:
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:60;
then t <= dw by A3, WAYBEL_0:66;
then A22: t c= dw by YELLOW_1:3;
2 in t by CARD_1:51, ENUMSET1:def 1;
then 2 in 2 by A22;
hence contradiction ; :: thesis:

end;

A23: now :: thesis:

assume B "/\" C = B ; :: thesis:
then B <= C by YELLOW_0:25;
then b <= c by YELLOW_0:60;
then td <= dw by A3, WAYBEL_0:66;
then A24: td c= dw by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
then 2 in 2 by A24;
hence contradiction ; :: thesis:

end;

A25: now :: thesis:

assume B "/\" C = C ; :: thesis:
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:60;
then dw <= td by A3, WAYBEL_0:66;
then A26: dw c= td by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A26, Th4, TARSKI:def 1; :: thesis:

end;

ex_inf_of {B,C},L by YELLOW_0:21;
then inf {B,C} in the carrier of K by YELLOW_0:def 16;
then B "/\" C in rng f by A6, YELLOW_0:40;
then ex x being object st
( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 3;
hence B "/\" C = A by A1, A23, A25, A19, A21, ENUMSET1:def 3; :: thesis:

end;

td <= tj by Lm1, YELLOW_1:3;
then b <= d by A3, WAYBEL_0:66;
then B <= D by YELLOW_0:59;
hence B "/\" D = B by YELLOW_0:25; :: thesis:
thus C "/\" D = A :: thesis:

proof

A27: now :: thesis:

assume C "/\" D = D ; :: thesis:
then D <= C by YELLOW_0:23;
then d <= c by YELLOW_0:60;
then tj <= dw by A3, WAYBEL_0:66;
then A28: tj c= dw by YELLOW_1:3;
2 in tj by Th3, TARSKI:def 2;
then 2 in 2 by A28;
hence contradiction ; :: thesis:

end;

A29: now :: thesis:

assume C "/\" D = E ; :: thesis:
then E <= C by YELLOW_0:23;
then e <= c by YELLOW_0:60;
then t <= dw by A3, WAYBEL_0:66;
then A30: t c= dw by YELLOW_1:3;
2 in t by CARD_1:51, ENUMSET1:def 1;
then 2 in 2 by A30;
hence contradiction ; :: thesis:

end;

A31: now :: thesis:

assume C "/\" D = B ; :: thesis:
then B <= C by YELLOW_0:23;
then b <= c by YELLOW_0:60;
then td <= dw by A3, WAYBEL_0:66;
then A32: td c= dw by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
then 2 in 2 by A32;
hence contradiction ; :: thesis:

end;

A33: now :: thesis:

assume C "/\" D = C ; :: thesis:
then C <= D by YELLOW_0:25;
then c <= d by YELLOW_0:60;
then dw <= tj by A3, WAYBEL_0:66;
then A34: dw c= tj by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A34, Th3, TARSKI:def 2; :: thesis:

end;

ex_inf_of {C,D},L by YELLOW_0:21;
then inf {C,D} in the carrier of K by YELLOW_0:def 16;
then C "/\" D in rng f by A6, YELLOW_0:40;
then ex x being object st
( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 3;
hence C "/\" D = A by A1, A31, A33, A27, A29, ENUMSET1:def 3; :: thesis:

end;

thus B "\/" C = E :: thesis:

proof

A35: now :: thesis:

assume B "\/" C = C ; :: thesis:
then C >= B by YELLOW_0:24;
then c >= b by YELLOW_0:60;
then dw >= td by A3, WAYBEL_0:66;
then A36: td c= dw by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
then 2 in 2 by A36;
hence contradiction ; :: thesis:

end;

A37: now :: thesis:

assume B "\/" C = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:60;
then tj >= dw by A3, WAYBEL_0:66;
then A38: dw c= tj by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A38, Th3, TARSKI:def 2; :: thesis:

end;

A39: now :: thesis:

assume B "\/" C = B ; :: thesis:
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:60;
then td >= dw by A3, WAYBEL_0:66;
then A40: dw c= td by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A40, Th4, TARSKI:def 1; :: thesis:

end;

A41: now :: thesis:

assume B "\/" C = A ; :: thesis:
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:60;
then z >= dw by A3, WAYBEL_0:66;
then dw c= z by YELLOW_1:3;
hence contradiction ; :: thesis:

end;

ex_sup_of {B,C},L by YELLOW_0:20;
then sup {B,C} in the carrier of K by YELLOW_0:def 17;
then B "\/" C in rng f by A6, YELLOW_0:41;
then ex x being object st
( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 3;
hence B "\/" C = E by A1, A39, A35, A37, A41, ENUMSET1:def 3; :: thesis:

end;

thus C "\/" D = E :: thesis:

proof

A42: now :: thesis:

assume C "\/" D = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:60;
then tj >= dw by A3, WAYBEL_0:66;
then A43: dw c= tj by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A43, Th3, TARSKI:def 2; :: thesis:

end;

A44: now :: thesis:

assume C "\/" D = C ; :: thesis:
then C >= D by YELLOW_0:24;
then c >= d by YELLOW_0:60;
then dw >= tj by A3, WAYBEL_0:66;
then A45: tj c= dw by YELLOW_1:3;
2 in tj by Th3, TARSKI:def 2;
hence contradiction by A45, CARD_1:50, TARSKI:def 2; :: thesis:

end;

A46: now :: thesis:

assume C "\/" D = B ; :: thesis:
then B >= C by YELLOW_0:22;
then b >= c by YELLOW_0:60;
then td >= dw by A3, WAYBEL_0:66;
then A47: dw c= td by YELLOW_1:3;
0 in dw by CARD_1:50, TARSKI:def 2;
hence contradiction by A47, Th4, TARSKI:def 1; :: thesis:

end;

A48: now :: thesis:

assume C "\/" D = A ; :: thesis:
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:60;
then z >= dw by A3, WAYBEL_0:66;
then dw c= z by YELLOW_1:3;
hence contradiction ; :: thesis:

end;

ex_sup_of {C,D},L by YELLOW_0:20;
then sup {C,D} in the carrier of K by YELLOW_0:def 17;
then C "\/" D in rng f by A6, YELLOW_0:41;
then ex x being object st
( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 3;
hence C "\/" D = E by A1, A46, A44, A42, A48, ENUMSET1:def 3; :: thesis:

end;

thus ( ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) implies ex K being full Sublattice of L st N_5 ,K are_isomorphic ) :: thesis:

proof

given a, b, c, d, e being Element of L such that AAA: a,b,c,d,e are_mutually_distinct and
A59: a "/\" b = a and
A60: a "/\" c = a and
A61: c "/\" e = c and
A62: d "/\" e = d and
A63: b "/\" c = a and
A64: b "/\" d = b and
A65: c "/\" d = a and
A66: b "\/" c = e and
A67: c "\/" d = e ; :: thesis:
set ck = {a,b,c,d,e};
reconsider ck = {a,b,c,d,e} as Subset of L ;
set K = subrelstr ck;
A68: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;
A69: subrelstr ck is meet-inheriting

proof

let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis:
assume that
A70: x in the carrier of (subrelstr ck) and
A71: y in the carrier of (subrelstr ck) and
ex_inf_of {x,y},L ; :: thesis:

per cases by A68, A70, A71, ENUMSET1:def 3;

suppose ( x = a & y = a ) ; :: thesis:

then inf {x,y} = a "/\" a by YELLOW_0:40;
then inf {x,y} = a by YELLOW_5:2;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = a & y = b ) ; :: thesis:

then inf {x,y} = a "/\" b by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = a & y = c ) ; :: thesis:

then inf {x,y} = a "/\" c by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A72: ( x = a & y = d ) ; :: thesis:

A73: b <= d by A64, YELLOW_0:25;
a <= b by A59, YELLOW_0:25;
then a <= d by A73, ORDERS_2:3;
then a "/\" d = a by YELLOW_0:25;
then inf {x,y} = a by A72, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A74: ( x = a & y = e ) ; :: thesis:

A75: c <= e by A61, YELLOW_0:25;
a <= c by A60, YELLOW_0:25;
then a <= e by A75, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A74, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = a ) ; :: thesis:

then inf {x,y} = a "/\" b by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = b ) ; :: thesis:

then inf {x,y} = b "/\" b by YELLOW_0:40;
then inf {x,y} = b by YELLOW_5:2;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = c ) ; :: thesis:

then inf {x,y} = b "/\" c by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = d ) ; :: thesis:

then inf {x,y} = b "/\" d by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A76: ( x = b & y = e ) ; :: thesis:

A77: d <= e by A62, YELLOW_0:25;
b <= d by A64, YELLOW_0:25;
then b <= e by A77, ORDERS_2:3;
then b "/\" e = b by YELLOW_0:25;
then inf {x,y} = b by A76, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = a ) ; :: thesis:

then inf {x,y} = a "/\" c by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = b ) ; :: thesis:

then inf {x,y} = b "/\" c by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = c ) ; :: thesis:

then inf {x,y} = c "/\" c by YELLOW_0:40;
then inf {x,y} = c by YELLOW_5:2;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = d ) ; :: thesis:

then inf {x,y} = c "/\" d by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = e ) ; :: thesis:

then inf {x,y} = c "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A78: ( x = d & y = a ) ; :: thesis:

A79: b <= d by A64, YELLOW_0:25;
a <= b by A59, YELLOW_0:25;
then a <= d by A79, ORDERS_2:3;
then a "/\" d = a by YELLOW_0:25;
then inf {x,y} = a by A78, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = b ) ; :: thesis:

then inf {x,y} = b "/\" d by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = c ) ; :: thesis:

then inf {x,y} = c "/\" d by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = d ) ; :: thesis:

then inf {x,y} = d "/\" d by YELLOW_0:40;
then inf {x,y} = d by YELLOW_5:2;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = e ) ; :: thesis:

then inf {x,y} = d "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A62, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A80: ( x = e & y = a ) ; :: thesis:

A81: c <= e by A61, YELLOW_0:25;
a <= c by A60, YELLOW_0:25;
then a <= e by A81, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A80, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A82: ( x = e & y = b ) ; :: thesis:

A83: d <= e by A62, YELLOW_0:25;
b <= d by A64, YELLOW_0:25;
then b <= e by A83, ORDERS_2:3;
then b "/\" e = b by YELLOW_0:25;
then inf {x,y} = b by A82, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = e & y = c ) ; :: thesis:

then inf {x,y} = c "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = e & y = d ) ; :: thesis:

then inf {x,y} = d "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A62, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = e & y = e ) ; :: thesis:

then inf {x,y} = e "/\" e by YELLOW_0:40;
then inf {x,y} = e by YELLOW_5:2;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

subrelstr ck is join-inheriting

proof

let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis:
assume that
A84: x in the carrier of (subrelstr ck) and
A85: y in the carrier of (subrelstr ck) and
ex_sup_of {x,y},L ; :: thesis:

per cases by A68, A84, A85, ENUMSET1:def 3;

suppose ( x = a & y = a ) ; :: thesis:

then sup {x,y} = a "\/" a by YELLOW_0:41;
then sup {x,y} = a by YELLOW_5:1;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = a & y = b ) ; :: thesis:

then x "\/" y = b by A59, Th5;
then sup {x,y} = b by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = a & y = c ) ; :: thesis:

then x "\/" y = c by A60, Th5;
then sup {x,y} = c by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A86: ( x = a & y = d ) ; :: thesis:

A87: b <= d by A64, YELLOW_0:25;
a <= b by A59, YELLOW_0:25;
then a <= d by A87, ORDERS_2:3;
then a "/\" d = a by YELLOW_0:25;
then a "\/" d = d by Th5;
then sup {x,y} = d by A86, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A88: ( x = a & y = e ) ; :: thesis:

A89: c <= e by A61, YELLOW_0:25;
a <= c by A60, YELLOW_0:25;
then a <= e by A89, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then a "\/" e = e by Th5;
then sup {x,y} = e by A88, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A90: ( x = b & y = a ) ; :: thesis:

a "\/" b = b by A59, Th5;
then sup {x,y} = b by A90, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = b ) ; :: thesis:

then sup {x,y} = b "\/" b by YELLOW_0:41;
then sup {x,y} = b by YELLOW_5:1;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = b & y = c ) ; :: thesis:

then sup {x,y} = b "\/" c by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A91: ( x = b & y = d ) ; :: thesis:

b "\/" d = d by A64, Th5;
then sup {x,y} = d by A91, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A92: ( x = b & y = e ) ; :: thesis:

A93: d <= e by A62, YELLOW_0:25;
b <= d by A64, YELLOW_0:25;
then b <= e by A93, ORDERS_2:3;
then b "/\" e = b by YELLOW_0:25;
then b "\/" e = e by Th5;
then sup {x,y} = e by A92, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A94: ( x = c & y = a ) ; :: thesis:

c "\/" a = c by A60, Th5;
then sup {x,y} = c by A94, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = b ) ; :: thesis:

then sup {x,y} = b "\/" c by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = c ) ; :: thesis:

then sup {x,y} = c "\/" c by YELLOW_0:41;
then sup {x,y} = c by YELLOW_5:1;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = c & y = d ) ; :: thesis:

then sup {x,y} = c "\/" d by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis:

end;

suppose A95: ( x = c & y = e ) ; :: thesis:

c "\/" e = e by A61, Th5;
then sup {x,y} = e by A95, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A96: ( x = d & y = a ) ; :: thesis:

A97: b <= d by A64, YELLOW_0:25;
a <= b by A59, YELLOW_0:25;
then a <= d by A97, ORDERS_2:3;
then a "/\" d = a by YELLOW_0:25;
then a "\/" d = d by Th5;
then sup {x,y} = d by A96, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A98: ( x = d & y = b ) ; :: thesis:

b "\/" d = d by A64, Th5;
then sup {x,y} = d by A98, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = c ) ; :: thesis:

then sup {x,y} = c "\/" d by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = d & y = d ) ; :: thesis:

then sup {x,y} = d "\/" d by YELLOW_0:41;
then sup {x,y} = d by YELLOW_5:1;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A99: ( x = d & y = e ) ; :: thesis:

d "\/" e = e by A62, Th5;
then sup {x,y} = e by A99, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A100: ( x = e & y = a ) ; :: thesis:

A101: c <= e by A61, YELLOW_0:25;
a <= c by A60, YELLOW_0:25;
then a <= e by A101, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then a "\/" e = e by Th5;
then sup {x,y} = e by A100, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A102: ( x = e & y = b ) ; :: thesis:

A103: d <= e by A62, YELLOW_0:25;
b <= d by A64, YELLOW_0:25;
then b <= e by A103, ORDERS_2:3;
then b "/\" e = b by YELLOW_0:25;
then b "\/" e = e by Th5;
then sup {x,y} = e by A102, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A104: ( x = e & y = c ) ; :: thesis:

c "\/" e = e by A61, Th5;
then sup {x,y} = e by A104, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose A105: ( x = e & y = d ) ; :: thesis:

d "\/" e = e by A62, Th5;
then sup {x,y} = e by A105, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

suppose ( x = e & y = e ) ; :: thesis:

then sup {x,y} = e "\/" e by YELLOW_0:41;
then sup {x,y} = e by YELLOW_5:1;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis:

end;

then reconsider K = subrelstr ck as non empty full Sublattice of L by A69, YELLOW_0:def 15;
take K ; :: thesis:
thus N_5 ,K are_isomorphic :: thesis:

proof

reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider td = 3 \ 2 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider dw = 2 as Element of N_5 by A1, ENUMSET1:def 3;

A106: now :: thesis:

assume A107: dw = td ; :: thesis:
2 in td by Th4, TARSKI:def 1;
hence contradiction by A107; :: thesis:

end;

A108: now :: thesis:

assume A109: td = t ; :: thesis:
not 1 in td by Th4, TARSKI:def 1;
hence contradiction by A109, CARD_1:51, ENUMSET1:def 1; :: thesis:

end;

reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;
defpred S₁[ object , object ] means for X being Element of N_5 st X = $1 holds
( ( X = z implies $2 = a ) & ( X = td implies $2 = b ) & ( X = dw implies $2 = c ) & ( X = tj implies $2 = d ) & ( X = t implies $2 = e ) );

A110: now :: thesis:

assume A111: tj = dw ; :: thesis:
2 in tj by Th3, TARSKI:def 2;
hence contradiction by A111; :: thesis:

end;

A112: now :: thesis:

assume A113: tj = t ; :: thesis:
not 0 in tj by Th3, TARSKI:def 2;
hence contradiction by A113, CARD_1:51, ENUMSET1:def 1; :: thesis:

end;

A114: now :: thesis:

assume A115: tj = td ; :: thesis:
not 1 in td by Th4, TARSKI:def 1;
hence contradiction by A115, Th3, TARSKI:def 2; :: thesis:

end;

A116: for x being object st x in the carrier of N_5 holds
ex y being object st
( y in ck & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A117: x in the carrier of N_5 ; :: thesis:

per cases by A1, A117, ENUMSET1:def 3;

suppose A118: x = 0 ; :: thesis:

take y = a; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of N_5; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A118, Th3, Th4; :: thesis:

end;

suppose A119: x = 3 \ 1 ; :: thesis:

take y = d; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of N_5; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A114, A112, A119, Th3; :: thesis:

end;

suppose A120: x = 2 ; :: thesis:

take y = c; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of N_5; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A106, A120; :: thesis:

end;

suppose A121: x = 3 \ 2 ; :: thesis:

take y = b; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of N_5; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A114, A106, A108, A121, Th4; :: thesis:

end;

suppose A122: x = 3 ; :: thesis:

take y = e; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of N_5; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A112, A108, A122; :: thesis:

end;