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

reconsider td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider j = 1 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider cl = the carrier of L as non empty set ;
reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;
given K being full Sublattice of L such that A2: M_3 ,K are_isomorphic ; :: thesis:
consider f being Function of M_3,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 M_3,ck ;
reconsider a = g . z, b = g . j, c = g . dj, d = g . td, 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, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis:
thus A <> C by A5, Th2, WAYBEL_1:def 1; :: thesis:
thus A <> D by A5, Th4, WAYBEL_1:def 1; :: thesis:
thus A <> E by A5, WAYBEL_1:def 1; :: thesis:

assume f . j = f . dj ; :: thesis:
then j = dj by A4, A5, WAYBEL_1:def 1;
then 1 in 1 by Th2, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

hence B <> C ; :: thesis:

now :: thesis:

assume f . j = f . td ; :: thesis:
then A11: j = td by A4, A5, WAYBEL_1:def 1;
0 in j by CARD_1:49, TARSKI:def 1;
hence contradiction by A11, Th4, TARSKI:def 1; :: thesis:

end;

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

now :: thesis:

assume f . dj = f . td ; :: thesis:
then A12: dj = td by A4, A5, WAYBEL_1:def 1;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A12, Th4, TARSKI:def 1; :: thesis:

end;

hence C <> D ; :: thesis:

now :: thesis:

assume f . dj = f . t ; :: thesis:
then A13: dj = t by A4, A5, WAYBEL_1:def 1;
0 in t by CARD_1:51, ENUMSET1:def 1;
hence contradiction by A13, Th2, TARSKI:def 1; :: thesis:

end;

hence C <> E ; :: thesis:

now :: thesis:

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dj ; :: thesis:
then x = 1 by Th2, TARSKI:def 1;
hence x in t by CARD_1:51, ENUMSET1:def 1; :: thesis:

end;

then dj <= t by YELLOW_1:3;
then c <= e by A3, WAYBEL_0:66;
then C <= E by YELLOW_0:59;
hence C "/\" E = C by YELLOW_0:25; :: thesis:
td <= t by YELLOW_1:3;
then d <= e by A3, WAYBEL_0:66;
then D <= E by YELLOW_0:59;
hence D "/\" E = D by YELLOW_0:25; :: thesis:
thus B "/\" C = A :: thesis:

proof

A15: now :: thesis:

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

end;

A17: now :: thesis:

assume B "/\" C = B ; :: thesis:
then B <= C by YELLOW_0:25;
then b <= c by YELLOW_0:60;
then j <= dj by A3, WAYBEL_0:66;
then A18: j c= dj by YELLOW_1:3;
0 in j by CARD_1:49, TARSKI:def 1;
hence contradiction by A18, Th2, TARSKI:def 1; :: thesis:

end;

A19: now :: thesis:

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

end;

A21: now :: thesis:

assume B "/\" C = C ; :: thesis:
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:60;
then dj <= j by A3, WAYBEL_0:66;
then A22: dj c= j by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A22, CARD_1:49, TARSKI:def 1; :: 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, A17, A21, A15, A19, ENUMSET1:def 3; :: thesis:

end;

thus B "/\" D = A :: thesis:

proof

A23: now :: thesis:

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

end;

A25: now :: thesis:

assume B "/\" D = C ; :: thesis:
then C <= B by YELLOW_0:23;
then c <= b by YELLOW_0:60;
then dj <= j by A3, WAYBEL_0:66;
then A26: dj c= j by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A26, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A27: now :: thesis:

assume B "/\" D = B ; :: thesis:
then B <= D by YELLOW_0:25;
then b <= d by YELLOW_0:60;
then j <= td by A3, WAYBEL_0:66;
then A28: j c= td by YELLOW_1:3;
0 in j by CARD_1:49, TARSKI:def 1;
hence contradiction by A28, Th4, TARSKI:def 1; :: thesis:

end;

A29: now :: thesis:

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

end;

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

end;

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

proof

A31: now :: thesis:

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

end;

A33: now :: thesis:

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

end;

A35: now :: thesis:

assume C "/\" D = C ; :: thesis:
then C <= D by YELLOW_0:25;
then c <= d by YELLOW_0:60;
then dj <= td by A3, WAYBEL_0:66;
then A36: dj c= td by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A36, Th4, TARSKI:def 1; :: thesis:

end;

A37: now :: thesis:

assume C "/\" D = B ; :: thesis:
then B <= C by YELLOW_0:23;
then b <= c by YELLOW_0:60;
then j <= dj by A3, WAYBEL_0:66;
then A38: j c= dj by YELLOW_1:3;
0 in j by CARD_1:49, TARSKI:def 1;
hence contradiction by A38, Th2, TARSKI:def 1; :: 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, A37, A35, A31, A33, ENUMSET1:def 3; :: thesis:

end;

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

proof

A39: now :: thesis:

assume B "\/" C = C ; :: thesis:
then C >= B by YELLOW_0:24;
then c >= b by YELLOW_0:60;
then dj >= j by A3, WAYBEL_0:66;
then A40: j c= dj by YELLOW_1:3;
0 in j by CARD_1:49, TARSKI:def 1;
hence contradiction by A40, Th2, TARSKI:def 1; :: thesis:

end;

A41: now :: thesis:

assume B "\/" C = B ; :: thesis:
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:60;
then j >= dj by A3, WAYBEL_0:66;
then A42: dj c= j by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A42, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A43: now :: thesis:

assume B "\/" C = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:60;
then td >= dj by A3, WAYBEL_0:66;
then A44: dj c= td by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A44, Th4, TARSKI:def 1; :: thesis:

end;

A45: now :: thesis:

assume B "\/" C = A ; :: thesis:
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:60;
then z >= dj by A3, WAYBEL_0:66;
then dj c= z by YELLOW_1:3;
hence contradiction by Th2; :: 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, A41, A39, A43, A45, ENUMSET1:def 3; :: thesis:

end;

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

proof

A46: now :: thesis:

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

end;

A48: now :: thesis:

assume B "\/" D = B ; :: thesis:
then B >= D by YELLOW_0:22;
then b >= d by YELLOW_0:60;
then j >= td by A3, WAYBEL_0:66;
then A49: td c= j by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
hence contradiction by A49, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A50: now :: thesis:

assume B "\/" D = C ; :: thesis:
then C >= D by YELLOW_0:22;
then c >= d by YELLOW_0:60;
then dj >= td by A3, WAYBEL_0:66;
then A51: td c= dj by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
hence contradiction by A51, Th2, TARSKI:def 1; :: thesis:

end;

A52: now :: thesis:

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

end;

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

end;

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

proof

A53: now :: thesis:

assume C "\/" D = B ; :: thesis:
then B >= C by YELLOW_0:22;
then b >= c by YELLOW_0:60;
then j >= dj by A3, WAYBEL_0:66;
then A54: dj c= j by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
then 1 in 1 by A54;
hence contradiction ; :: thesis:

end;

A55: now :: thesis:

assume C "\/" D = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:60;
then td >= dj by A3, WAYBEL_0:66;
then A56: dj c= td by YELLOW_1:3;
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A56, Th4, TARSKI:def 1; :: thesis:

end;

A57: now :: thesis:

assume C "\/" D = C ; :: thesis:
then C >= D by YELLOW_0:24;
then c >= d by YELLOW_0:60;
then dj >= td by A3, WAYBEL_0:66;
then A58: td c= dj by YELLOW_1:3;
2 in td by Th4, TARSKI:def 1;
hence contradiction by A58, Th2, TARSKI:def 1; :: thesis:

end;

A59: now :: thesis:

assume C "\/" D = A ; :: thesis:
then A >= C by YELLOW_0:22;
then a >= c by YELLOW_0:60;
then z >= dj by A3, WAYBEL_0:66;
then dj c= z by YELLOW_1:3;
hence contradiction by Th2; :: 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, A53, A57, A55, A59, 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 & 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 ) :: thesis:

proof

given a, b, c, d, e being Element of L such that AAA: a,b,c,d,e are_mutually_distinct and
A70: a "/\" b = a and
A71: a "/\" c = a and
A72: a "/\" d = a and
A73: b "/\" e = b and
A74: c "/\" e = c and
A75: d "/\" e = d and
A76: b "/\" c = a and
A77: b "/\" d = a and
A78: c "/\" d = a and
A79: b "\/" c = e and
A80: b "\/" d = e and
A81: c "\/" d = e ; :: thesis:
set ck = {a,b,c,d,e};
reconsider ck = {a,b,c,d,e} as Subset of L ;
set K = subrelstr ck;
A82: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;
A83: subrelstr ck is meet-inheriting

proof

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

per cases by A82, A84, A85, 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 A82, 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 A70, A82, 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 A71, A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

A87: c <= e by A74, YELLOW_0:25;
a <= c by A71, YELLOW_0:25;
then a <= e by A87, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A86, YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A82, 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 A70, A82, 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 A82, 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 A76, A82, 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 A77, A82, ENUMSET1:def 3; :: thesis:

end;

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

then inf {x,y} = b "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, 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 A71, A82, 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 A76, A82, 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 A82, 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 A78, A82, 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 A74, A82, ENUMSET1:def 3; :: thesis:

end;

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

then inf {x,y} = a "/\" d by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A72, A82, 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 A77, A82, 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 A78, A82, 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 A82, 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 A75, A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

then inf {x,y} = b "/\" e by YELLOW_0:40;
hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A73, A82, 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 A74, A82, 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 A75, A82, 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 A82, 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
A90: x in the carrier of (subrelstr ck) and
A91: y in the carrier of (subrelstr ck) and
ex_sup_of {x,y},L ; :: thesis:

per cases by A82, A90, A91, 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 A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

A93: c <= e by A74, YELLOW_0:25;
a <= c by A71, YELLOW_0:25;
then a <= e by A93, ORDERS_2:3;
then a "/\" e = a by YELLOW_0:25;
then a "\/" e = e by Th5;
then sup {x,y} = e by A92, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, ENUMSET1:def 3; :: thesis:

end;

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

a "\/" b = b by A70, Th5;
then sup {x,y} = b by A94, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, 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 A82, 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 A79, A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

c "\/" a = c by A71, Th5;
then sup {x,y} = c by A96, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, 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 A79, A82, 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 A82, 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 A81, A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

then sup {x,y} = b "\/" d by YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A80, A82, 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 A81, A82, 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 A82, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

d "\/" e = e by A75, Th5;
then sup {x,y} = e by A103, YELLOW_0:41;
hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A82, 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 A82, ENUMSET1:def 3; :: thesis:

end;

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

proof

reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider dj = 2 \ 1 as Element of M_3 by A1, ENUMSET1:def 3;

A104: now :: thesis:

A105: 2 in t by CARD_1:51, ENUMSET1:def 1;
assume dj = t ; :: thesis:
hence contradiction by A105, Th2, TARSKI:def 1; :: thesis:

end;

A106: now :: thesis:

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

end;

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

A108: now :: thesis:

assume A109: j = dj ; :: thesis:
1 in dj by Th2, TARSKI:def 1;
hence contradiction by A109; :: thesis:

end;

A110: now :: thesis:

assume A111: j = td ; :: thesis:
2 in td by Th4, TARSKI:def 1;
hence contradiction by A111, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A112: now :: thesis:

assume A113: dj = td ; :: thesis:
2 in td by Th4, TARSKI:def 1;
hence contradiction by A113, Th2, TARSKI:def 1; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume A115: x in the carrier of M_3 ; :: thesis:

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

suppose A116: x = 0 ; :: thesis:

take y = a; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of M_3; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A116, Th2, Th4; :: thesis:

end;

suppose A117: x = 1 ; :: thesis:

take y = b; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of M_3; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A110, A117; :: thesis:

end;

suppose A118: x = 2 \ 1 ; :: thesis:

take y = c; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of M_3; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A108, A112, A104, A118, Th2; :: thesis:

end;

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

take y = d; :: thesis:
thus y in ck by ENUMSET1:def 3; :: thesis:
let X be Element of M_3; :: thesis:
thus ( X = x implies ( ( X = z implies y = a ) & ( X = j implies y = b ) & ( X = dj implies y = c ) & ( X = td implies y = d ) & ( X = t implies y = e ) ) ) by A110, A112, A106, A119, Th4; :: thesis:

end;

suppose A120: x = 3 ; :: thesis:

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

end;