let L be LATTICE; :: thesis:
set cn = the carrier of N_5 ;
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 & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ) :: thesis:

proof

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, 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 N_5 by A1, ENUMSET1:def 3;
reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;
reconsider dw = 2 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 t = 3 as Element of N_5 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 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;
( 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, Th4, WAYBEL_1:def 1; :: 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:

now

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

end;

hence B <> C ; :: thesis:

now

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

end;

hence B <> D ; :: thesis:

now

assume A9: f . td = f . t ; :: thesis:
( not 1 in td & 1 in t ) by Th4, CARD_1:89, ENUMSET1:def 1, TARSKI:def 1;
hence contradiction by A4, A5, A9, WAYBEL_1:def 1; :: thesis:

end;

hence B <> E ; :: thesis:

now

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

end;

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

now

assume A11: f . tj = f . t ; :: thesis:
( not 0 in tj & 0 in t ) by Th3, CARD_1:89, ENUMSET1:def 1, TARSKI:def 2;
hence contradiction by A4, A5, A11, WAYBEL_1:def 1; :: thesis:

end;

hence D <> E ; :: thesis:
z c= td by XBOOLE_1:2;
then z <= td 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= dw by XBOOLE_1:2;
then z <= dw 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:
dw c= t by NAT_1:40;
then dw <= 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:
tj <= 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
A12: ( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 5;

A13: now

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

end;

A15: now

assume B "/\" C = C ; :: thesis:
then C <= B by YELLOW_0:25;
then c <= b by YELLOW_0:61;
then dw <= td by A3, WAYBEL_0:66;
then A16: dw c= td by YELLOW_1:3;
( 0 in dw & 0 <> 2 ) by CARD_1:88, TARSKI:def 2;
hence contradiction by A16, Th4, TARSKI:def 1; :: thesis:

end;

A17: now

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

end;

now

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

end;

hence B "/\" C = A by A1, A12, A13, A15, A17, 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:60;
hence B "/\" D = B by YELLOW_0:25; :: thesis:
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
A20: ( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 5;

A21: now

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

end;

A23: now

assume C "/\" D = C ; :: thesis:
then C <= D by YELLOW_0:25;
then c <= d by YELLOW_0:61;
then dw <= tj by A3, WAYBEL_0:66;
then A24: dw c= tj by YELLOW_1:3;
( 0 in dw & 0 <> 2 & 0 <> 1 ) by CARD_1:88, TARSKI:def 2;
hence contradiction by A24, Th3, TARSKI:def 2; :: thesis:

end;

A25: now

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

end;

now

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

end;

hence C "/\" D = A by A1, A20, A21, A23, A25, 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
A28: ( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 5;

A29: now

assume B "\/" C = B ; :: thesis:
then B >= C by YELLOW_0:24;
then b >= c by YELLOW_0:61;
then td >= dw by A3, WAYBEL_0:66;
then A30: dw c= td by YELLOW_1:3;
( 0 in dw & 0 <> 2 ) by CARD_1:88, TARSKI:def 2;
hence contradiction by A30, Th4, TARSKI:def 1; :: thesis:

end;

A31: now

assume B "\/" C = C ; :: thesis:
then C >= B by YELLOW_0:24;
then c >= b by YELLOW_0:61;
then dw >= td 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

assume B "\/" C = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then tj >= dw by A3, WAYBEL_0:66;
then A34: dw c= tj by YELLOW_1:3;
( 0 in dw & 0 <> 1 & 0 <> 2 ) by CARD_1:88, TARSKI:def 2;
hence contradiction by A34, Th3, TARSKI:def 2; :: thesis:

end;

now

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

end;

hence B "\/" C = E by A1, A28, A29, A31, A33, 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
A35: ( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 5;

A36: now

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

end;

A38: now

assume C "\/" D = C ; :: thesis:
then C >= D by YELLOW_0:24;
then c >= d by YELLOW_0:61;
then dw >= tj by A3, WAYBEL_0:66;
then A39: tj c= dw by YELLOW_1:3;
( 2 in tj & 2 <> 0 & 2 <> 1 ) by Th3, TARSKI:def 2;
hence contradiction by A39, CARD_1:88, TARSKI:def 2; :: thesis:

end;

A40: now

assume C "\/" D = D ; :: thesis:
then D >= C by YELLOW_0:22;
then d >= c by YELLOW_0:61;
then tj >= dw by A3, WAYBEL_0:66;
then A41: dw c= tj by YELLOW_1:3;
( 0 in dw & 0 <> 1 & 0 <> 2 ) by CARD_1:88, TARSKI:def 2;
hence contradiction by A41, Th3, TARSKI:def 2; :: thesis:

end;

now

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

end;

hence C "\/" D = E by A1, A35, A36, A38, A40, 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 & 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 A42: ( a <> b & a <> c & a <> d & a <> e & b <> c & b <> d & b <> e & c <> d & c <> e & d <> e & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ; :: thesis:
set ck = {a,b,c,d,e};
reconsider ck = {a,b,c,d,e} as Subset of L ;
set K = subrelstr ck;
A43: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;
A44: subrelstr ck is meet-inheriting

proof

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

per cases by A43, A45, 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 A43, 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 A42, A43, 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 A42, A43, ENUMSET1:def 3; :: thesis:

end;

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

( a <= b & b <= d ) by A42, YELLOW_0:25;
then a <= d by ORDERS_2:26;
then a "/\" d = a by YELLOW_0:25;
then inf {x,y} = a by A46, YELLOW_0:40;
hence "/\" {x,y},L in the carrier of (subrelstr ck) by A43, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

( a <= c & c <= e ) by A42, YELLOW_0:25;
then a <= e by ORDERS_2:26;
then a "/\" e = a by YELLOW_0:25;
then inf {x,y} = a by A50, YELLOW_0:40;
hence "/\" {x,y},L in the carrier of (subrelstr ck) by A43, ENUMSET1:def 3; :: thesis:

end;

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

( b <= d & d <= e ) by A42, YELLOW_0:25;
then b <= e by ORDERS_2:26;
then b "/\" e = b by YELLOW_0:25;
then inf {x,y} = b by A51, YELLOW_0:40;
hence "/\" {x,y},L in the carrier of (subrelstr ck) by A43, 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 A42, A43, 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 A42, A43, 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 A43, 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 A52: ( x in the carrier of (subrelstr ck) & y in the carrier of (subrelstr ck) & ex_sup_of {x,y},L ) ; :: thesis:

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

end;

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

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

end;

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

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

end;

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

( a <= b & b <= d ) by A42, YELLOW_0:25;
then a <= d by ORDERS_2:26;
then a "/\" d = a by YELLOW_0:25;
then a "\/" d = d by Th5;
then sup {x,y} = d by A53, YELLOW_0:41;
hence "\/" {x,y},L in the carrier of (subrelstr ck) by A43, ENUMSET1:def 3; :: thesis:

end;

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

( a <= c & c <= e ) by A42, 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 A54, YELLOW_0:41;
hence "\/" {x,y},L in the carrier of (subrelstr ck) by A43, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

( a <= b & b <= d ) by A42, YELLOW_0:25;
then a <= d by ORDERS_2:26;
then a "/\" d = a by YELLOW_0:25;
then a "\/" d = d by Th5;
then sup {x,y} = d by A60, YELLOW_0:41;
hence "\/" {x,y},L in the carrier of (subrelstr ck) by A43, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

( a <= c & c <= e ) by A42, 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 A43, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

then reconsider K = subrelstr ck as non empty full Sublattice of L by A43, A44;
take K ; :: thesis:
thus N_5 ,K are_isomorphic :: thesis:

proof

reconsider z = 0 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 dw = 2 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 t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

A67: now

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

end;

A69: now

assume A70: tj = td ; :: thesis:
( not 1 in td & 1 in tj ) by Th3, Th4, TARSKI:def 1, TARSKI:def 2;
hence contradiction by A70; :: thesis:

end;

A71: now

assume A72: tj = t ; :: thesis:
( not 0 in tj & 0 in t ) by Th3, CARD_1:89, ENUMSET1:def 1, TARSKI:def 2;
hence contradiction by A72; :: thesis:

end;

A73: now

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

end;

A75: now

assume A76: td = t ; :: thesis:
( not 1 in td & 1 in t ) by Th4, CARD_1:89, ENUMSET1:def 1, TARSKI:def 1;
hence contradiction by A76; :: thesis:

end;

defpred S₁[ set , set ] means for X being Element of N_5 st X = $1 holds
( ( X = z implies $2 = a ) & ( X = td implies $2 = b ) & ( X = dw implies $2 = c ) & ( X = tj implies $2 = d ) & ( X = t implies $2 = e ) );
A77: for x being set st x in the carrier of N_5 holds
ex y being set st
( y in ck & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A78: x in the carrier of N_5 ; :: thesis:

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

suppose A79: 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 A79, Th3, Th4; :: thesis:

end;

suppose A80: 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 A67, A69, A71, A80, Th3; :: thesis:

end;

suppose A81: 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 A67, A73, A81; :: thesis:

end;

suppose A82: 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 A69, A73, A75, A82, Th4; :: thesis:

end;

suppose A83: 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 A71, A75, A83; :: thesis:

end;

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

proof

now

let x, y be Element of N_5 ; :: thesis:
assume A86: 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 = tj & y = tj ) ; :: thesis:

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

hence x = y ; :: thesis:

end;

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

then ( f . x = a & f . y = d ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = a & f . y = c ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = a & f . y = b ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = a & f . y = e ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = d & f . y = a ) by A84;
hence x = y by A42, A86; :: thesis:

end;

suppose ( x = tj & y = dw ) ; :: thesis:

then ( f . x = d & f . y = c ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = d & f . y = b ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = d & f . y = e ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = c & f . y = a ) by A84;
hence x = y by A42, A86; :: thesis:

end;

suppose ( x = dw & y = tj ) ; :: thesis:

then ( f . x = c & f . y = d ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = c & f . y = b ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = c & f . y = e ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = b & f . y = a ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = b & f . y = d ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = b & f . y = c ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = b & f . y = e ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = e & f . y = a ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = e & f . y = d ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = e & f . y = c ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

then ( f . x = e & f . y = b ) by A84;
hence x = y by A42, A86; :: thesis:

end;

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

end;

A87: dom f = the carrier of N_5 by FUNCT_2:def 1;
A88: 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
A89: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of N_5 by A89;
( x = z or x = tj or x = dw 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 A84, A89;
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 A90: y in ck ; :: thesis:

per cases by A90, ENUMSET1:def 3;

suppose A91: y = a ; :: thesis:

( z in dom f & a = f . z ) by A84, A87;
hence y in rng f by A91, FUNCT_1:def 5; :: thesis:

end;

suppose A92: y = b ; :: thesis:

( td in dom f & b = f . td ) by A84, A87;
hence y in rng f by A92, FUNCT_1:def 5; :: thesis:

end;

suppose A93: y = c ; :: thesis:

( dw in dom f & c = f . dw ) by A84, A87;
hence y in rng f by A93, FUNCT_1:def 5; :: thesis:

end;

suppose A94: y = d ; :: thesis:

( tj in dom f & d = f . tj ) by A84, A87;
hence y in rng f by A94, FUNCT_1:def 5; :: thesis:

end;

suppose A95: y = e ; :: thesis:

( t in dom f & e = f . t ) by A84, A87;
hence y in rng f by A95, FUNCT_1:def 5; :: thesis:

end;

for x, y being Element of N_5 holds
( x <= y iff f . x <= f . y )

proof

let x, y be Element of N_5 ; :: thesis:
thus ( x <= y implies f . x <= f . y ) :: thesis:

proof

assume A96: 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 = td ) ; :: thesis:

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

end;

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

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

end;

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

then A99: ( f . x = a & f . y = d ) by A84;
reconsider A = a, D = d as Element of K by A43, ENUMSET1:def 3;
( a <= b & b <= d ) by A42, YELLOW_0:25;
then ( a <= d & A in the carrier of K & D in the carrier of K ) by ORDERS_2:26;
hence f . x <= f . y by A99, YELLOW_0:61; :: thesis:

end;

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

then A100: ( f . x = a & f . y = e ) by A84;
reconsider A = a, E = e as Element of K by A43, ENUMSET1:def 3;
( a <= c & c <= e ) by A42, 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 A100, YELLOW_0:61; :: thesis:

end;

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

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

end;

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

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

end;

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

( 2 in td & not 2 in dw ) by Th4, TARSKI:def 1;
then not td c= dw ;
hence f . x <= f . y by A96, A101, YELLOW_1:3; :: thesis:

end;

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

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

end;

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

then A102: ( f . x = b & f . y = d ) by A84;
reconsider D = d, B = b as Element of K by A43, ENUMSET1:def 3;
( b <= d & B in the carrier of K & D in the carrier of K ) by A42, YELLOW_0:25;
hence f . x <= f . y by A102, YELLOW_0:61; :: thesis:

end;

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

then A103: ( f . x = b & f . y = e ) by A84;
reconsider B = b, E = e as Element of K by A43, ENUMSET1:def 3;
( b <= d & d <= e ) by A42, YELLOW_0:25;
then ( b <= e & B in the carrier of K & E in the carrier of K ) by ORDERS_2:26;
hence f . x <= f . y by A103, YELLOW_0:61; :: thesis:

end;

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

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

end;

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

( 0 in dw & not 0 in td ) by Th4, CARD_1:88, TARSKI:def 1, TARSKI:def 2;
then not dw c= td ;
hence f . x <= f . y by A96, A104, YELLOW_1:3; :: thesis:

end;

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

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

end;

suppose A105: ( x = dw & y = tj ) ; :: thesis:

( 0 in dw & not 0 in tj ) by Th3, CARD_1:88, TARSKI:def 2;
then not dw c= tj ;
hence f . x <= f . y by A96, A105, YELLOW_1:3; :: thesis:

end;

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

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

end;

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

then tj c= z by A96, YELLOW_1:3;
hence f . x <= f . y by Th3; :: thesis:

end;

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

( 1 in tj & not 1 in td ) by Th3, Th4, TARSKI:def 1, TARSKI:def 2;
then not tj c= td ;
hence f . x <= f . y by A96, A107, YELLOW_1:3; :: thesis:

end;

suppose A108: ( x = tj & y = dw ) ; :: thesis:

( 2 in tj & not 2 in dw ) by Th3, TARSKI:def 2;
then not tj c= dw ;
hence f . x <= f . y by A96, A108, YELLOW_1:3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

suppose A110: ( 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 A96, A110, YELLOW_1:3; :: thesis:

end;

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

( 2 in t & not 2 in dw ) by CARD_1:89, ENUMSET1:def 1;
then not t c= dw ;
hence f . x <= f . y by A96, A111, YELLOW_1:3; :: thesis:

end;

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

( 0 in t & not 0 in tj ) by Th3, CARD_1:89, ENUMSET1:def 1, TARSKI:def 2;
then not t c= tj ;
hence f . x <= f . y by A96, A112, 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 A113: f . x <= f . y ; :: thesis:
A114: ( f . x in ck & f . y in ck ) by A87, A88, FUNCT_1:def 5;

per cases by A114, ENUMSET1:def 3;

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

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

end;

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

( f . z = a & f . td = b ) by A84;
then ( z = x & td = y ) by A85, A115, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . z = a & f . dw = c ) by A84;
then ( z = x & dw = y ) by A85, A116, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . z = a & f . tj = d ) by A84;
then ( z = x & tj = y ) by A85, A117, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:2;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . z = a & f . t = e ) by A84;
then ( z = x & t = y ) by A85, A118, 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 A113, YELLOW_0:60;
hence x <= y by A42, YELLOW_0:25; :: thesis:

end;

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

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

end;

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

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

end;

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

( f . td = b & f . tj = d ) by A84;
then ( x = td & y = tj & 1 c= 2 ) by A85, A119, NAT_1:40, WAYBEL_1:def 1;
then x c= y by XBOOLE_1:34;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

( f . td = b & f . t = e ) by A84;
then ( td = x & t = y ) by A85, A120, WAYBEL_1:def 1;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

A122: dw c= t

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in dw ; :: thesis:
then ( X = 0 or X = 1 ) by CARD_1:88, TARSKI:def 2;
hence X in t by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

( f . dw = c & f . t = e ) by A84;
then ( dw = x & t = y ) by A85, A121, WAYBEL_1:def 1;
hence x <= y by A122, YELLOW_1:3; :: thesis:

end;

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

then ( d <= a & a <= b ) by A42, A113, YELLOW_0:25, YELLOW_0:60;
then d <= b by ORDERS_2:26;
hence x <= y by A42, YELLOW_0:25; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

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

( f . tj = d & f . t = e ) by A84;
then ( tj = x & t = y ) by A85, A123, WAYBEL_1:def 1;
hence x <= y by YELLOW_1:3; :: thesis:

end;

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

then A124: e <= a by A113, YELLOW_0:60;
( a <= b & b <= d & d <= e ) by A42, YELLOW_0:25;
then ( a <= d & d <= e ) by ORDERS_2:26;
then a <= e by ORDERS_2:26;
hence x <= y by A42, A124, ORDERS_2:25; :: thesis:

end;

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

then A125: e <= b by A113, YELLOW_0:60;
( b <= d & d <= e ) by A42, YELLOW_0:25;
then b <= e by ORDERS_2:26;
hence x <= y by A42, A125, ORDERS_2:25; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

hence f is isomorphic by A43, A85, A88, WAYBEL_0:66; :: thesis:

end;