let L be LATTICE; :: thesis:
set cn = the carrier of M_3 ;
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 & 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 ) ) :: thesis:

proof

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, WAYBEL_1:def 8;
A4: not K is empty by A3, WAYBEL_0:def 38;
reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;
A5: ( f is one-to-one & f is monotone ) by A3, A4, WAYBEL_0:def 38;
reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider j = 1 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 td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider cl = the carrier of L as non empty set ;
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;
( 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 ; :: thesis:
take B ; :: thesis:
take C ; :: thesis:
take D ; :: thesis:
take E ; :: thesis:
thus A <> B by A5, WAYBEL_1:def 1; :: 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:

now

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

assume f . j = f . td ; :: thesis:
then A7: j = td by A4, A5, WAYBEL_1:def 1;
( 0 in j & 0 <> 2 ) by CARD_1:87, TARSKI:def 1;
hence contradiction by A7, Th4, TARSKI:def 1; :: thesis:

end;

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

now

assume f . dj = f . td ; :: thesis:
then A8: dj = td by A4, A5, WAYBEL_1:def 1;
( 1 in dj & 1 <> 2 ) by Th2, TARSKI:def 1;
hence contradiction by A8, Th4, TARSKI:def 1; :: thesis:

end;

hence C <> D ; :: thesis:

now

assume f . dj = f . t ; :: thesis:
then A9: dj = t by A4, A5, WAYBEL_1:def 1;
( 0 in t & 0 <> 1 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A9, Th2, TARSKI:def 1; :: thesis:

end;

hence C <> E ; :: thesis:

now

assume f . td = f . t ; :: thesis:
then A10: td = t by A4, A5, WAYBEL_1:def 1;
( 0 in t & 0 <> 2 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A10, Th4, TARSKI:def 1; :: thesis:

end;

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

proof

let x be set ; :: 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:89, 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:60;
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:60;
hence D "/\" E = D by YELLOW_0:25; :: thesis:
thus B "/\" C = A :: thesis:

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 A6, YELLOW_0:40;
then consider x being set such that
A11: ( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 5;

A12: now

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

end;

A14: now

assume B "/\" C = C ; :: thesis:
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:61;
then dj <= j by A3, WAYBEL_0:66;
then A15: dj c= j by YELLOW_1:3;
( 1 in dj & 0 <> 1 ) by Th2, TARSKI:def 1;
hence contradiction by A15, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A16: now

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

end;

now

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

end;

hence B "/\" C = A by A1, A11, A12, A14, A16, ENUMSET1:def 3; :: thesis:

end;

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

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 A6, YELLOW_0:40;
then consider x being set such that
A19: ( x in dom f & B "/\" D = f . x ) by FUNCT_1:def 5;

A20: now

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

end;

A22: now

assume B "/\" D = C ; :: thesis:
then C <= B by YELLOW_0:23;
then c <= b by YELLOW_0:61;
then dj <= j by A3, WAYBEL_0:66;
then A23: dj c= j by YELLOW_1:3;
( 1 in dj & 0 <> 1 ) by Th2, TARSKI:def 1;
hence contradiction by A23, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A24: now

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

end;

now

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

end;

hence B "/\" D = A by A1, A19, A20, A22, A24, ENUMSET1:def 3; :: thesis:

end;

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

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 A6, YELLOW_0:40;
then consider x being set such that
A27: ( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 5;

A28: now

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

end;

A30: now

assume C "/\" D = C ; :: thesis:
then C <= D by YELLOW_0:25;
then c <= d by YELLOW_0:61;
then dj <= td by A3, WAYBEL_0:66;
then A31: dj c= td by YELLOW_1:3;
( 1 in dj & 1 <> 2 ) by Th2, TARSKI:def 1;
hence contradiction by A31, Th4, TARSKI:def 1; :: thesis:

end;

A32: now

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

end;

now

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

end;

hence C "/\" D = A by A1, A27, A28, A30, A32, ENUMSET1:def 3; :: thesis:

end;

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

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 A6, YELLOW_0:41;
then consider x being set such that
A35: ( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 5;

A36: now

assume B "\/" C = B ; :: thesis:
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:61;
then j >= dj by A3, WAYBEL_0:66;
then A37: dj c= j by YELLOW_1:3;
( 1 in dj & 0 <> 1 ) by Th2, TARSKI:def 1;
hence contradiction by A37, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A38: now

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

end;

A40: now

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

end;

now

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

end;

hence B "\/" C = E by A1, A35, A36, A38, A40, ENUMSET1:def 3; :: thesis:

end;

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

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 A6, YELLOW_0:41;
then consider x being set such that
A42: ( x in dom f & B "\/" D = f . x ) by FUNCT_1:def 5;

A43: now

assume B "\/" D = B ; :: thesis:
then B >= D by YELLOW_0:22;
then b >= d by YELLOW_0:61;
then j >= td by A3, WAYBEL_0:66;
then A44: td c= j by YELLOW_1:3;
( 2 in td & 2 <> 0 ) by Th4, TARSKI:def 1;
hence contradiction by A44, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A45: now

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

end;

A47: now

assume B "\/" D = D ; :: thesis:
then D >= B by YELLOW_0:22;
then d >= b by YELLOW_0:61;
then td >= j by A3, WAYBEL_0:66;
then A48: j c= td by YELLOW_1:3;
( 0 in j & 0 <> 2 ) by CARD_1:87, TARSKI:def 1;
hence contradiction by A48, Th4, TARSKI:def 1; :: thesis:

end;

now

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

end;

hence B "\/" D = E by A1, A42, A43, A45, A47, ENUMSET1:def 3; :: thesis:

end;

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

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 A6, YELLOW_0:41;
then consider x being set such that
A49: ( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 5;

A50: now

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

end;

A52: now

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

end;

A54: now

assume C "\/" D = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then td >= dj by A3, WAYBEL_0:66;
then A55: dj c= td by YELLOW_1:3;
( 1 in dj & 1 <> 2 ) by Th2, TARSKI:def 1;
hence contradiction by A55, Th4, TARSKI:def 1; :: thesis:

end;

now

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

end;

hence C "\/" D = E by A1, A49, A50, A52, A54, ENUMSET1:def 3; :: thesis:

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 ) :: thesis:

proof

given a, b, c, d, e being Element of L such that A56: ( 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 ) ; :: thesis:
set ck = {a,b,c,d,e};
reconsider ck = {a,b,c,d,e} as Subset of L ;
set K = subrelstr ck;
A57: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;
A58: subrelstr ck is meet-inheriting

proof

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

per cases by A57, A59, 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 A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, ENUMSET1:def 3; :: thesis:

end;

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

( a <= c & c <= e ) by A56, YELLOW_0:25;
then a <= e by ORDERS_2:26;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A60, YELLOW_0:40;
hence "/\" {x,y},L in the carrier of (subrelstr ck) by A57, 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 A56, A57, 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 A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A57, 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 A56, A57, ENUMSET1:def 3; :: thesis:

end;

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

( a <= c & c <= e ) by A56, YELLOW_0:25;
then a <= e by ORDERS_2:26;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A61, YELLOW_0:40;
hence "/\" {x,y},L in the carrier of (subrelstr ck) by A57, 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 A56, A57, 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 A56, A57, 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 A56, A57, 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 A57, 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 A62: ( x in the carrier of (subrelstr ck) & y in the carrier of (subrelstr ck) & ex_sup_of {x,y},L ) ; :: thesis:

per cases by A57, A62, 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 A57, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

( a <= c & c <= e ) by A56, YELLOW_0:25;
then a <= e by ORDERS_2:26;
then a "/\" e = a by YELLOW_0:25;
then a "\/" e = e by Th5;
then sup {x,y} = e by A63, YELLOW_0:41;
hence "\/" {x,y},L in the carrier of (subrelstr ck) by A57, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

( a <= c & c <= e ) by A56, YELLOW_0:25;
then a <= e by ORDERS_2:26;
then a "/\" e = a by YELLOW_0:25;
then a "\/" e = e by Th5;
then sup {x,y} = e by A69, YELLOW_0:41;
hence "\/" {x,y},L in the carrier of (subrelstr ck) by A57, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

then reconsider K = subrelstr ck as non empty full Sublattice of L by A57, A58;
take K ; :: thesis:
thus M_3 ,K are_isomorphic :: thesis:

proof

reconsider z = 0 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider j = 1 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 td = 3 \ 2 as Element of M_3 by A1, ENUMSET1:def 3;
reconsider t = 3 as Element of M_3 by A1, ENUMSET1:def 3;

A73: now

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

end;

A75: now

assume A76: j = td ; :: thesis:
( 2 in td & 0 <> 2 ) by Th4, TARSKI:def 1;
hence contradiction by A76, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A77: now

assume A78: dj = td ; :: thesis:
( 2 in td & 1 <> 2 ) by Th4, TARSKI:def 1;
hence contradiction by A78, Th2, TARSKI:def 1; :: thesis:

end;

A79: now

assume A80: dj = t ; :: thesis:
( 2 in t & 1 <> 2 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A80, Th2, TARSKI:def 1; :: thesis:

end;

A81: now

assume A82: td = t ; :: thesis:
( 0 in t & 0 <> 2 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A82, Th4, TARSKI:def 1; :: thesis:

end;

defpred S₁[ 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 ) );
A83: for x being set st x in the carrier of M_3 holds
ex y being set st
( y in ck & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A84: x in the carrier of M_3 ; :: thesis:

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

suppose A85: 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 A85, Th2, Th4; :: thesis:

end;

suppose A86: 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 A73, A75, A86; :: thesis:

end;

suppose A87: 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 A73, A77, A79, A87, Th2; :: thesis:

end;

suppose A88: 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 A75, A77, A81, A88, Th4; :: thesis:

end;

suppose A89: 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 A79, A81, A89; :: thesis:

end;

consider f being Function of the carrier of M_3 ,ck such that
A90: for x being set st x in the carrier of M_3 holds
S₁[x,f . x] from FUNCT_2:sch 1(A83);
reconsider f = f as Function of M_3 ,K by A57;
take f ; :: according to WAYBEL_1:def 8 :: thesis:
A91: f is one-to-one

proof

now

let x, y be Element of M_3 ; :: thesis:
assume A92: f . x = f . y ; :: thesis:
thus x = y :: thesis:

proof

per cases by A1, ENUMSET1:def 3;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

suppose ( x = z & y = j ) ; :: thesis:

then ( f . x = a & f . y = b ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = z & y = dj ) ; :: thesis:

then ( f . x = a & f . y = c ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = z & y = td ) ; :: thesis:

then ( f . x = a & f . y = d ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = z & y = t ) ; :: thesis:

then ( f . x = a & f . y = e ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = j & y = z ) ; :: thesis:

then ( f . x = b & f . y = a ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = j & y = dj ) ; :: thesis:

then ( f . x = b & f . y = c ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = j & y = td ) ; :: thesis:

then ( f . x = b & f . y = d ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = j & y = t ) ; :: thesis:

then ( f . x = b & f . y = e ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = dj & y = z ) ; :: thesis:

then ( f . x = c & f . y = a ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = dj & y = j ) ; :: thesis:

then ( f . x = c & f . y = b ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = dj & y = td ) ; :: thesis:

then ( f . x = c & f . y = d ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = dj & y = t ) ; :: thesis:

then ( f . x = c & f . y = e ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = td & y = z ) ; :: thesis:

then ( f . x = d & f . y = a ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = td & y = j ) ; :: thesis:

then ( f . x = d & f . y = b ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = td & y = dj ) ; :: thesis:

then ( f . x = d & f . y = c ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = td & y = t ) ; :: thesis:

then ( f . x = d & f . y = e ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = t & y = z ) ; :: thesis:

then ( f . x = e & f . y = a ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = t & y = j ) ; :: thesis:

then ( f . x = e & f . y = b ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = t & y = dj ) ; :: thesis:

then ( f . x = e & f . y = c ) by A90;
hence x = y by A56, A92; :: thesis:

end;

suppose ( x = t & y = td ) ; :: thesis:

then ( f . x = e & f . y = d ) by A90;
hence x = y by A56, A92; :: thesis:

end;

hence f is one-to-one by WAYBEL_1:def 1; :: thesis:

end;

A93: dom f = the carrier of M_3 by FUNCT_2:def 1;
A94: rng f = ck

proof

thus rng f c= ck :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A95: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of M_3 by A95;
( x = z or x = j or x = dj or x = td or x = t ) by A1, ENUMSET1:def 3;
then ( y = a or y = d or y = c or y = b or y = e ) by A90, A95;
hence y in ck by ENUMSET1:def 3; :: thesis:

end;

thus ck c= rng f :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A96: y in ck ; :: thesis:

per cases by A96, ENUMSET1:def 3;

suppose A97: y = a ; :: thesis:

( z in dom f & a = f . z ) by A90, A93;
hence y in rng f by A97, FUNCT_1:def 5; :: thesis:

end;

suppose A98: y = b ; :: thesis:

( j in dom f & b = f . j ) by A90, A93;
hence y in rng f by A98, FUNCT_1:def 5; :: thesis:

end;

suppose A99: y = c ; :: thesis:

( dj in dom f & c = f . dj ) by A90, A93;
hence y in rng f by A99, FUNCT_1:def 5; :: thesis:

end;

suppose A100: y = d ; :: thesis:

( td in dom f & d = f . td ) by A90, A93;
hence y in rng f by A100, FUNCT_1:def 5; :: thesis:

end;

suppose A101: y = e ; :: thesis:

( t in dom f & e = f . t ) by A90, A93;
hence y in rng f by A101, FUNCT_1:def 5; :: thesis:

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 ; :: thesis:
thus ( x <= y implies f . x <= f . y ) :: thesis:

proof

assume A102: x <= y ; :: thesis:

per cases by A1, ENUMSET1:def 3;

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

hence f . x <= f . y ; :: thesis:

end;

suppose ( x = z & y = j ) ; :: thesis:

then A103: ( f . x = a & f . y = b ) by A90;
reconsider A = a, B = b as Element of K by A57, ENUMSET1:def 3;
( a <= b & A in the carrier of K & B in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A103, YELLOW_0:61; :: thesis:

end;

suppose ( x = z & y = dj ) ; :: thesis:

then A104: ( f . x = a & f . y = c ) by A90;
reconsider A = a, C = c as Element of K by A57, ENUMSET1:def 3;
( a <= c & A in the carrier of K & C in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A104, YELLOW_0:61; :: thesis:

end;

suppose ( x = z & y = td ) ; :: thesis:

then A105: ( f . x = a & f . y = d ) by A90;
reconsider A = a, D = d as Element of K by A57, ENUMSET1:def 3;
( a <= d & A in the carrier of K & D in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A105, YELLOW_0:61; :: thesis:

end;

suppose ( x = z & y = t ) ; :: thesis:

then A106: ( f . x = a & f . y = e ) by A90;
reconsider A = a, E = e as Element of K by A57, ENUMSET1:def 3;
( a <= c & c <= e ) by A56, YELLOW_0:25;
then ( a <= e & A in the carrier of K & E in the carrier of K ) by ORDERS_2:26;
hence f . x <= f . y by A106, YELLOW_0:61; :: thesis:

end;

suppose ( x = j & y = z ) ; :: thesis:

then j c= z by A102, YELLOW_1:3;
hence f . x <= f . y ; :: thesis:

end;

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

hence f . x <= f . y ; :: thesis:

end;

suppose A107: ( x = j & y = dj ) ; :: thesis:

( 0 in j & not 0 in dj ) by Th2, CARD_1:87, TARSKI:def 1;
then not j c= dj ;
hence f . x <= f . y by A102, A107, YELLOW_1:3; :: thesis:

end;

suppose A108: ( x = j & y = td ) ; :: thesis:

( 0 in j & not 0 in td ) by Th4, CARD_1:87, TARSKI:def 1;
then not j c= td ;
hence f . x <= f . y by A102, A108, YELLOW_1:3; :: thesis:

end;

suppose ( x = j & y = t ) ; :: thesis:

then A109: ( f . x = b & f . y = e ) by A90;
reconsider B = b, E = e as Element of K by A57, ENUMSET1:def 3;
( b <= e & B in the carrier of K & E in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A109, YELLOW_0:61; :: thesis:

end;

suppose ( x = dj & y = z ) ; :: thesis:

then dj c= z by A102, YELLOW_1:3;
hence f . x <= f . y by Th2; :: thesis:

end;

suppose A110: ( x = dj & y = j ) ; :: thesis:

( 1 in dj & not 1 in j ) by Th2, TARSKI:def 1;
then not dj c= j ;
hence f . x <= f . y by A102, A110, YELLOW_1:3; :: thesis:

end;

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

hence f . x <= f . y ; :: thesis:

end;

suppose A111: ( x = dj & y = td ) ; :: thesis:

( 1 in dj & not 1 in td ) by Th2, Th4, TARSKI:def 1;
then not dj c= td ;
hence f . x <= f . y by A102, A111, YELLOW_1:3; :: thesis:

end;

suppose ( x = dj & y = t ) ; :: thesis:

then A112: ( f . x = c & f . y = e ) by A90;
reconsider C = c, E = e as Element of K by A57, ENUMSET1:def 3;
( c <= e & C in the carrier of K & E in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A112, YELLOW_0:61; :: thesis:

end;

suppose ( x = td & y = z ) ; :: thesis:

then td c= z by A102, YELLOW_1:3;
hence f . x <= f . y by Th4; :: thesis:

end;

suppose A113: ( x = td & y = j ) ; :: thesis:

( 2 in td & not 2 in j ) by Th4, CARD_1:87, TARSKI:def 1;
then not td c= j ;
hence f . x <= f . y by A102, A113, YELLOW_1:3; :: thesis:

end;

suppose A114: ( x = td & y = dj ) ; :: thesis:

( 2 in td & not 2 in dj ) by Th2, Th4, TARSKI:def 1;
then not td c= dj ;
hence f . x <= f . y by A102, A114, YELLOW_1:3; :: thesis:

end;

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

hence f . x <= f . y ; :: thesis:

end;

suppose ( x = td & y = t ) ; :: thesis:

then A115: ( f . x = d & f . y = e ) by A90;
reconsider D = d, E = e as Element of K by A57, ENUMSET1:def 3;
( d <= e & D in the carrier of K & E in the carrier of K ) by A56, YELLOW_0:25;
hence f . x <= f . y by A115, YELLOW_0:61; :: thesis:

end;

suppose ( x = t & y = z ) ; :: thesis:

then t c= z by A102, YELLOW_1:3;
hence f . x <= f . y ; :: thesis:

end;

suppose A116: ( x = t & y = j ) ; :: thesis:

( 1 in t & not 1 in j ) by CARD_1:89, ENUMSET1:def 1;
then not t c= j ;
hence f . x <= f . y by A102, A116, YELLOW_1:3; :: thesis:

end;

suppose A117: ( x = t & y = dj ) ; :: thesis:

( 2 in t & not 2 in dj ) by Th2, CARD_1:89, ENUMSET1:def 1, TARSKI:def 1;
then not t c= dj ;
hence f . x <= f . y by A102, A117, YELLOW_1:3; :: thesis:

end;

suppose A118: ( x = t & y = td ) ; :: thesis:

( 0 in t & not 0 in td ) by Th4, CARD_1:89, ENUMSET1:def 1, TARSKI:def 1;
then not t c= td ;
hence f . x <= f . y by A102, A118, YELLOW_1:3; :: thesis:

end;

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

hence f . x <= f . y ; :: thesis:

end;

thus ( f . x <= f . y implies x <= y ) :: thesis:

proof

assume A119: f . x <= f . y ; :: thesis:
A120: ( f . x in ck & f . y in ck ) by A93, A94, FUNCT_1:def 5;
A121: dj c= t

proof

let X be set ; :: 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:89, ENUMSET1:def 1; :: thesis:

end;

per cases by A120, ENUMSET1:def 3;

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

hence x <= y by A91, WAYBEL_1:def 1; :: thesis:

end;

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

( f . z = a & f . j = b ) by A90;
then ( z = x & j = y ) by A91, A122, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . z = a & f . dj = c ) by A90;
then ( z = x & dj = y ) by A91, A123, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . z = a & f . td = d ) by A90;
then ( z = x & td = y ) by A91, A124, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

suppose A125: ( f . x = a & f . y = e ) ; :: thesis:

( f . z = a & f . t = e ) by A90;
then ( z = x & t = y ) by A91, A125, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

then b <= a by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

hence x <= y by A91, WAYBEL_1:def 1; :: thesis:

end;

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

then b <= c by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then b <= d by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

( f . j = b & f . t = e ) by A90;
then ( j = x & t = y ) by A91, A126, WAYBEL_1:def 1;
then x c= y by NAT_1:40;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

then c <= a by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then c <= b by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

hence x <= y by A91, WAYBEL_1:def 1; :: thesis:

end;

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

then c <= d by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

( f . dj = c & f . t = e ) by A90;
then ( dj = x & t = y ) by A91, A127, WAYBEL_1:def 1;
hence x <= y by A121, YELLOW_1:3; :: thesis:

end;

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

then ( d <= a & a <= b ) by A56, A119, YELLOW_0:25, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then d <= b by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then d <= c by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

hence x <= y by A91, WAYBEL_1:def 1; :: thesis:

end;

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

( f . td = d & f . t = e ) by A90;
then ( td = x & t = y ) by A91, A128, WAYBEL_1:def 1;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

then ( e <= a & a <= b ) by A56, A119, YELLOW_0:25, YELLOW_0:60;
then e <= b by ORDERS_2:26;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then e <= b by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then e <= c by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

then e <= d by A119, YELLOW_0:60;
hence x <= y by A56, YELLOW_0:25; :: thesis:

end;

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

hence x <= y by A91, WAYBEL_1:def 1; :: thesis:

end;

hence f is isomorphic by A57, A91, A94, WAYBEL_0:66; :: thesis:

end;