set cn = the carrier of N_5;

let L be LATTICE; :: thesis: ( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) )

A1: the carrier of N_5 = {0,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

thus ( ex K being full Sublattice of L st N_5 ,K are_isomorphic implies ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ) :: thesis: ( ex a, b, c, d, e being Element of L st

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

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

let L be LATTICE; :: thesis: ( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) )

A1: the carrier of N_5 = {0,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

thus ( ex K being full Sublattice of L st N_5 ,K are_isomorphic implies ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) ) :: thesis: ( ex a, b, c, d, e being Element of L st

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

proof

thus
( ex a, b, c, d, e being Element of L st
reconsider td = 3 \ 2 as Element of N_5 by A1, ENUMSET1:def 3;

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

reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;

reconsider cl = the carrier of L as non empty set ;

reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

given K being full Sublattice of L such that A2: N_5 ,K are_isomorphic ; :: thesis: ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e )

consider f being Function of N_5,K such that

A3: f is isomorphic by A2;

A4: not K is empty by A3, WAYBEL_0:def 38;

then A5: ( f is one-to-one & f is monotone ) by A3, WAYBEL_0:def 38;

reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

reconsider ck = the carrier of K as non empty set ;

A6: ck = rng f by A3, WAYBEL_0:66;

reconsider g = f as Function of the carrier of N_5,ck ;

reconsider a = g . z, b = g . td, c = g . dw, d = g . tj, e = g . t as Element of K ;

reconsider ck = ck as non empty Subset of cl by YELLOW_0:def 13;

A7: b in ck ;

A8: c in ck ;

A9: e in ck ;

A10: d in ck ;

a in ck ;

then reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

take A ; :: thesis: ex b, c, d, e being Element of L st

( A,b,c,d,e are_mutually_distinct & A "/\" b = A & A "/\" c = A & c "/\" e = c & d "/\" e = d & b "/\" c = A & b "/\" d = b & c "/\" d = A & b "\/" c = e & c "\/" d = e )

take B ; :: thesis: ex c, d, e being Element of L st

( A,B,c,d,e are_mutually_distinct & A "/\" B = A & A "/\" c = A & c "/\" e = c & d "/\" e = d & B "/\" c = A & B "/\" d = B & c "/\" d = A & B "\/" c = e & c "\/" d = e )

take C ; :: thesis: ex d, e being Element of L st

( A,B,C,d,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" e = C & d "/\" e = d & B "/\" C = A & B "/\" d = B & C "/\" d = A & B "\/" C = e & C "\/" d = e )

take D ; :: thesis: ex e being Element of L st

( A,B,C,D,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" e = C & D "/\" e = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = e & C "\/" D = e )

take E ; :: thesis: ( A,B,C,D,E are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus A <> B by A5, Th4, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis: ( not A = C & not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> C by A5, WAYBEL_1:def 1; :: thesis: ( not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> D by A5, Th3, WAYBEL_1:def 1; :: thesis: ( not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> E by A5, WAYBEL_1:def 1; :: thesis: ( not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus C <> E by A5, WAYBEL_1:def 1; :: thesis: ( not 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 )

z c= td ;

then z <= td by YELLOW_1:3;

then a <= b by A3, WAYBEL_0:66;

then A <= B by YELLOW_0:59;

hence A "/\" B = A by YELLOW_0:25; :: thesis: ( A "/\" C = A & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

z c= dw ;

then z <= dw by YELLOW_1:3;

then a <= c by A3, WAYBEL_0:66;

then A <= C by YELLOW_0:59;

hence A "/\" C = A by YELLOW_0:25; :: thesis: ( C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

Segm 2 c= Segm 3 by NAT_1:39;

then dw <= t by YELLOW_1:3;

then c <= e by A3, WAYBEL_0:66;

then C <= E by YELLOW_0:59;

hence C "/\" E = C by YELLOW_0:25; :: thesis: ( D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

tj <= t by YELLOW_1:3;

then d <= e by A3, WAYBEL_0:66;

then D <= E by YELLOW_0:59;

hence D "/\" E = D by YELLOW_0:25; :: thesis: ( B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus B "/\" C = A :: thesis: ( B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

then b <= d by A3, WAYBEL_0:66;

then B <= D by YELLOW_0:59;

hence B "/\" D = B by YELLOW_0:25; :: thesis: ( C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus C "/\" D = A :: thesis: ( B "\/" C = E & C "\/" D = E )

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

reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;

reconsider cl = the carrier of L as non empty set ;

reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

given K being full Sublattice of L such that A2: N_5 ,K are_isomorphic ; :: thesis: ex a, b, c, d, e being Element of L st

( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e )

consider f being Function of N_5,K such that

A3: f is isomorphic by A2;

A4: not K is empty by A3, WAYBEL_0:def 38;

then A5: ( f is one-to-one & f is monotone ) by A3, WAYBEL_0:def 38;

reconsider K = K as non empty SubRelStr of L by A3, WAYBEL_0:def 38;

reconsider ck = the carrier of K as non empty set ;

A6: ck = rng f by A3, WAYBEL_0:66;

reconsider g = f as Function of the carrier of N_5,ck ;

reconsider a = g . z, b = g . td, c = g . dw, d = g . tj, e = g . t as Element of K ;

reconsider ck = ck as non empty Subset of cl by YELLOW_0:def 13;

A7: b in ck ;

A8: c in ck ;

A9: e in ck ;

A10: d in ck ;

a in ck ;

then reconsider A = a, B = b, C = c, D = d, E = e as Element of L by A7, A8, A10, A9;

take A ; :: thesis: ex b, c, d, e being Element of L st

( A,b,c,d,e are_mutually_distinct & A "/\" b = A & A "/\" c = A & c "/\" e = c & d "/\" e = d & b "/\" c = A & b "/\" d = b & c "/\" d = A & b "\/" c = e & c "\/" d = e )

take B ; :: thesis: ex c, d, e being Element of L st

( A,B,c,d,e are_mutually_distinct & A "/\" B = A & A "/\" c = A & c "/\" e = c & d "/\" e = d & B "/\" c = A & B "/\" d = B & c "/\" d = A & B "\/" c = e & c "\/" d = e )

take C ; :: thesis: ex d, e being Element of L st

( A,B,C,d,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" e = C & d "/\" e = d & B "/\" C = A & B "/\" d = B & C "/\" d = A & B "\/" C = e & C "\/" d = e )

take D ; :: thesis: ex e being Element of L st

( A,B,C,D,e are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" e = C & D "/\" e = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = e & C "\/" D = e )

take E ; :: thesis: ( A,B,C,D,E are_mutually_distinct & A "/\" B = A & A "/\" C = A & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus A <> B by A5, Th4, WAYBEL_1:def 1; :: according to ZFMISC_1:def 7 :: thesis: ( not A = C & not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> C by A5, WAYBEL_1:def 1; :: thesis: ( not A = D & not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> D by A5, Th3, WAYBEL_1:def 1; :: thesis: ( not A = E & not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

thus A <> E by A5, WAYBEL_1:def 1; :: thesis: ( not B = C & not B = D & not B = E & not C = D & not C = E & not 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 )

now :: thesis: not f . td = f . dw

hence
B <> C
; :: thesis: ( not B = D & not B = E & not C = D & not C = E & not 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 )assume
f . td = f . dw
; :: thesis: contradiction

then A11: td = dw by A4, A5, WAYBEL_1:def 1;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A11; :: thesis: verum

end;then A11: td = dw by A4, A5, WAYBEL_1:def 1;

2 in td by Th4, TARSKI:def 1;

hence contradiction by A11; :: thesis: verum

now :: thesis: not f . td = f . tj

hence
B <> D
; :: thesis: ( not B = E & not C = D & not C = E & not 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 )A12:
1 in tj
by Th3, TARSKI:def 2;

assume A13: f . td = f . tj ; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A4, A5, A13, A12, WAYBEL_1:def 1; :: thesis: verum

end;assume A13: f . td = f . tj ; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A4, A5, A13, A12, WAYBEL_1:def 1; :: thesis: verum

now :: thesis: not f . td = f . t

hence
B <> E
; :: thesis: ( not C = D & not C = E & not 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 )A14:
1 in t
by CARD_1:51, ENUMSET1:def 1;

assume A15: f . td = f . t ; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A4, A5, A15, A14, WAYBEL_1:def 1; :: thesis: verum

end;assume A15: f . td = f . t ; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A4, A5, A15, A14, WAYBEL_1:def 1; :: thesis: verum

now :: thesis: not f . dw = f . tj

hence
C <> D
; :: thesis: ( not C = E & not 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 )assume
f . dw = f . tj
; :: thesis: contradiction

then A16: dw = tj by A4, A5, WAYBEL_1:def 1;

2 in tj by Th3, TARSKI:def 2;

hence contradiction by A16; :: thesis: verum

end;then A16: dw = tj by A4, A5, WAYBEL_1:def 1;

2 in tj by Th3, TARSKI:def 2;

hence contradiction by A16; :: thesis: verum

thus C <> E by A5, WAYBEL_1:def 1; :: thesis: ( not 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 )

now :: thesis: not f . tj = f . t

hence
D <> E
; :: thesis: ( 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 )A17:
0 in t
by CARD_1:51, ENUMSET1:def 1;

assume A18: f . tj = f . t ; :: thesis: contradiction

not 0 in tj by Th3, TARSKI:def 2;

hence contradiction by A4, A5, A18, A17, WAYBEL_1:def 1; :: thesis: verum

end;assume A18: f . tj = f . t ; :: thesis: contradiction

not 0 in tj by Th3, TARSKI:def 2;

hence contradiction by A4, A5, A18, A17, WAYBEL_1:def 1; :: thesis: verum

z c= td ;

then z <= td by YELLOW_1:3;

then a <= b by A3, WAYBEL_0:66;

then A <= B by YELLOW_0:59;

hence A "/\" B = A by YELLOW_0:25; :: thesis: ( A "/\" C = A & C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

z c= dw ;

then z <= dw by YELLOW_1:3;

then a <= c by A3, WAYBEL_0:66;

then A <= C by YELLOW_0:59;

hence A "/\" C = A by YELLOW_0:25; :: thesis: ( C "/\" E = C & D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

Segm 2 c= Segm 3 by NAT_1:39;

then dw <= t by YELLOW_1:3;

then c <= e by A3, WAYBEL_0:66;

then C <= E by YELLOW_0:59;

hence C "/\" E = C by YELLOW_0:25; :: thesis: ( D "/\" E = D & B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

tj <= t by YELLOW_1:3;

then d <= e by A3, WAYBEL_0:66;

then D <= E by YELLOW_0:59;

hence D "/\" E = D by YELLOW_0:25; :: thesis: ( B "/\" C = A & B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus B "/\" C = A :: thesis: ( B "/\" D = B & C "/\" D = A & B "\/" C = E & C "\/" D = E )

proof

then inf {B,C} in the carrier of K by YELLOW_0:def 16;

then B "/\" C in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 3;

hence B "/\" C = A by A1, A23, A25, A19, A21, ENUMSET1:def 3; :: thesis: verum

end;

td <= tj
by Lm1, YELLOW_1:3;A19: now :: thesis: not B "/\" C = D

assume
B "/\" C = D
; :: thesis: contradiction

then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then tj <= dw by A3, WAYBEL_0:66;

then A20: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

then 2 in 2 by A20;

hence contradiction ; :: thesis: verum

end;then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then tj <= dw by A3, WAYBEL_0:66;

then A20: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

then 2 in 2 by A20;

hence contradiction ; :: thesis: verum

A21: now :: thesis: not B "/\" C = E

assume
B "/\" C = E
; :: thesis: contradiction

then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dw by A3, WAYBEL_0:66;

then A22: t c= dw by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

then 2 in 2 by A22;

hence contradiction ; :: thesis: verum

end;then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dw by A3, WAYBEL_0:66;

then A22: t c= dw by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

then 2 in 2 by A22;

hence contradiction ; :: thesis: verum

A23: now :: thesis: not B "/\" C = B

assume
B "/\" C = B
; :: thesis: contradiction

then B <= C by YELLOW_0:25;

then b <= c by YELLOW_0:60;

then td <= dw by A3, WAYBEL_0:66;

then A24: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A24;

hence contradiction ; :: thesis: verum

end;then B <= C by YELLOW_0:25;

then b <= c by YELLOW_0:60;

then td <= dw by A3, WAYBEL_0:66;

then A24: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A24;

hence contradiction ; :: thesis: verum

A25: now :: thesis: not B "/\" C = C

ex_inf_of {B,C},L
by YELLOW_0:21;assume
B "/\" C = C
; :: thesis: contradiction

then C <= B by YELLOW_0:25;

then c <= b by YELLOW_0:60;

then dw <= td by A3, WAYBEL_0:66;

then A26: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A26, Th4, TARSKI:def 1; :: thesis: verum

end;then C <= B by YELLOW_0:25;

then c <= b by YELLOW_0:60;

then dw <= td by A3, WAYBEL_0:66;

then A26: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A26, Th4, TARSKI:def 1; :: thesis: verum

then inf {B,C} in the carrier of K by YELLOW_0:def 16;

then B "/\" C in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & B "/\" C = f . x ) by FUNCT_1:def 3;

hence B "/\" C = A by A1, A23, A25, A19, A21, ENUMSET1:def 3; :: thesis: verum

then b <= d by A3, WAYBEL_0:66;

then B <= D by YELLOW_0:59;

hence B "/\" D = B by YELLOW_0:25; :: thesis: ( C "/\" D = A & B "\/" C = E & C "\/" D = E )

thus C "/\" D = A :: thesis: ( B "\/" C = E & C "\/" D = E )

proof

then inf {C,D} in the carrier of K by YELLOW_0:def 16;

then C "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 3;

hence C "/\" D = A by A1, A31, A33, A27, A29, ENUMSET1:def 3; :: thesis: verum

end;

thus
B "\/" C = E
:: thesis: C "\/" D = EA27: now :: thesis: not C "/\" D = D

assume
C "/\" D = D
; :: thesis: contradiction

then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then tj <= dw by A3, WAYBEL_0:66;

then A28: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

then 2 in 2 by A28;

hence contradiction ; :: thesis: verum

end;then D <= C by YELLOW_0:23;

then d <= c by YELLOW_0:60;

then tj <= dw by A3, WAYBEL_0:66;

then A28: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

then 2 in 2 by A28;

hence contradiction ; :: thesis: verum

A29: now :: thesis: not C "/\" D = E

assume
C "/\" D = E
; :: thesis: contradiction

then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dw by A3, WAYBEL_0:66;

then A30: t c= dw by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

then 2 in 2 by A30;

hence contradiction ; :: thesis: verum

end;then E <= C by YELLOW_0:23;

then e <= c by YELLOW_0:60;

then t <= dw by A3, WAYBEL_0:66;

then A30: t c= dw by YELLOW_1:3;

2 in t by CARD_1:51, ENUMSET1:def 1;

then 2 in 2 by A30;

hence contradiction ; :: thesis: verum

A31: now :: thesis: not C "/\" D = B

assume
C "/\" D = B
; :: thesis: contradiction

then B <= C by YELLOW_0:23;

then b <= c by YELLOW_0:60;

then td <= dw by A3, WAYBEL_0:66;

then A32: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A32;

hence contradiction ; :: thesis: verum

end;then B <= C by YELLOW_0:23;

then b <= c by YELLOW_0:60;

then td <= dw by A3, WAYBEL_0:66;

then A32: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A32;

hence contradiction ; :: thesis: verum

A33: now :: thesis: not C "/\" D = C

ex_inf_of {C,D},L
by YELLOW_0:21;assume
C "/\" D = C
; :: thesis: contradiction

then C <= D by YELLOW_0:25;

then c <= d by YELLOW_0:60;

then dw <= tj by A3, WAYBEL_0:66;

then A34: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A34, Th3, TARSKI:def 2; :: thesis: verum

end;then C <= D by YELLOW_0:25;

then c <= d by YELLOW_0:60;

then dw <= tj by A3, WAYBEL_0:66;

then A34: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A34, Th3, TARSKI:def 2; :: thesis: verum

then inf {C,D} in the carrier of K by YELLOW_0:def 16;

then C "/\" D in rng f by A6, YELLOW_0:40;

then ex x being object st

( x in dom f & C "/\" D = f . x ) by FUNCT_1:def 3;

hence C "/\" D = A by A1, A31, A33, A27, A29, ENUMSET1:def 3; :: thesis: verum

proof

then sup {B,C} in the carrier of K by YELLOW_0:def 17;

then B "\/" C in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 3;

hence B "\/" C = E by A1, A39, A35, A37, A41, ENUMSET1:def 3; :: thesis: verum

end;

thus
C "\/" D = E
:: thesis: verumA35: now :: thesis: not B "\/" C = C

assume
B "\/" C = C
; :: thesis: contradiction

then C >= B by YELLOW_0:24;

then c >= b by YELLOW_0:60;

then dw >= td by A3, WAYBEL_0:66;

then A36: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A36;

hence contradiction ; :: thesis: verum

end;then C >= B by YELLOW_0:24;

then c >= b by YELLOW_0:60;

then dw >= td by A3, WAYBEL_0:66;

then A36: td c= dw by YELLOW_1:3;

2 in td by Th4, TARSKI:def 1;

then 2 in 2 by A36;

hence contradiction ; :: thesis: verum

A37: now :: thesis: not B "\/" C = D

assume
B "\/" C = D
; :: thesis: contradiction

then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then tj >= dw by A3, WAYBEL_0:66;

then A38: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A38, Th3, TARSKI:def 2; :: thesis: verum

end;then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then tj >= dw by A3, WAYBEL_0:66;

then A38: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A38, Th3, TARSKI:def 2; :: thesis: verum

A39: now :: thesis: not B "\/" C = B

assume
B "\/" C = B
; :: thesis: contradiction

then B >= C by YELLOW_0:24;

then b >= c by YELLOW_0:60;

then td >= dw by A3, WAYBEL_0:66;

then A40: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A40, Th4, TARSKI:def 1; :: thesis: verum

end;then B >= C by YELLOW_0:24;

then b >= c by YELLOW_0:60;

then td >= dw by A3, WAYBEL_0:66;

then A40: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A40, Th4, TARSKI:def 1; :: thesis: verum

A41: now :: thesis: not B "\/" C = A

ex_sup_of {B,C},L
by YELLOW_0:20;assume
B "\/" C = A
; :: thesis: contradiction

then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dw by A3, WAYBEL_0:66;

then dw c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

end;then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dw by A3, WAYBEL_0:66;

then dw c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

then sup {B,C} in the carrier of K by YELLOW_0:def 17;

then B "\/" C in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & B "\/" C = f . x ) by FUNCT_1:def 3;

hence B "\/" C = E by A1, A39, A35, A37, A41, ENUMSET1:def 3; :: thesis: verum

proof

then sup {C,D} in the carrier of K by YELLOW_0:def 17;

then C "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 3;

hence C "\/" D = E by A1, A46, A44, A42, A48, ENUMSET1:def 3; :: thesis: verum

end;

A42: now :: thesis: not C "\/" D = D

assume
C "\/" D = D
; :: thesis: contradiction

then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then tj >= dw by A3, WAYBEL_0:66;

then A43: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A43, Th3, TARSKI:def 2; :: thesis: verum

end;then D >= C by YELLOW_0:22;

then d >= c by YELLOW_0:60;

then tj >= dw by A3, WAYBEL_0:66;

then A43: dw c= tj by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A43, Th3, TARSKI:def 2; :: thesis: verum

A44: now :: thesis: not C "\/" D = C

assume
C "\/" D = C
; :: thesis: contradiction

then C >= D by YELLOW_0:24;

then c >= d by YELLOW_0:60;

then dw >= tj by A3, WAYBEL_0:66;

then A45: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

hence contradiction by A45, CARD_1:50, TARSKI:def 2; :: thesis: verum

end;then C >= D by YELLOW_0:24;

then c >= d by YELLOW_0:60;

then dw >= tj by A3, WAYBEL_0:66;

then A45: tj c= dw by YELLOW_1:3;

2 in tj by Th3, TARSKI:def 2;

hence contradiction by A45, CARD_1:50, TARSKI:def 2; :: thesis: verum

A46: now :: thesis: not C "\/" D = B

assume
C "\/" D = B
; :: thesis: contradiction

then B >= C by YELLOW_0:22;

then b >= c by YELLOW_0:60;

then td >= dw by A3, WAYBEL_0:66;

then A47: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A47, Th4, TARSKI:def 1; :: thesis: verum

end;then B >= C by YELLOW_0:22;

then b >= c by YELLOW_0:60;

then td >= dw by A3, WAYBEL_0:66;

then A47: dw c= td by YELLOW_1:3;

0 in dw by CARD_1:50, TARSKI:def 2;

hence contradiction by A47, Th4, TARSKI:def 1; :: thesis: verum

A48: now :: thesis: not C "\/" D = A

ex_sup_of {C,D},L
by YELLOW_0:20;assume
C "\/" D = A
; :: thesis: contradiction

then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dw by A3, WAYBEL_0:66;

then dw c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

end;then A >= C by YELLOW_0:22;

then a >= c by YELLOW_0:60;

then z >= dw by A3, WAYBEL_0:66;

then dw c= z by YELLOW_1:3;

hence contradiction ; :: thesis: verum

then sup {C,D} in the carrier of K by YELLOW_0:def 17;

then C "\/" D in rng f by A6, YELLOW_0:41;

then ex x being object st

( x in dom f & C "\/" D = f . x ) by FUNCT_1:def 3;

hence C "\/" D = E by A1, A46, A44, A42, A48, ENUMSET1:def 3; :: thesis: verum

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

proof

given a, b, c, d, e being Element of L such that AAA:
a,b,c,d,e are_mutually_distinct
and

A59: a "/\" b = a and

A60: a "/\" c = a and

A61: c "/\" e = c and

A62: d "/\" e = d and

A63: b "/\" c = a and

A64: b "/\" d = b and

A65: c "/\" d = a and

A66: b "\/" c = e and

A67: c "\/" d = e ; :: thesis: ex K being full Sublattice of L st N_5 ,K are_isomorphic

set ck = {a,b,c,d,e};

reconsider ck = {a,b,c,d,e} as Subset of L ;

set K = subrelstr ck;

A68: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;

A69: subrelstr ck is meet-inheriting

take K ; :: thesis: N_5 ,K are_isomorphic

thus N_5 ,K are_isomorphic :: thesis: verum

end;A59: a "/\" b = a and

A60: a "/\" c = a and

A61: c "/\" e = c and

A62: d "/\" e = d and

A63: b "/\" c = a and

A64: b "/\" d = b and

A65: c "/\" d = a and

A66: b "\/" c = e and

A67: c "\/" d = e ; :: thesis: ex K being full Sublattice of L st N_5 ,K are_isomorphic

set ck = {a,b,c,d,e};

reconsider ck = {a,b,c,d,e} as Subset of L ;

set K = subrelstr ck;

A68: the carrier of (subrelstr ck) = ck by YELLOW_0:def 15;

A69: subrelstr ck is meet-inheriting

proof

subrelstr ck is join-inheriting
let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of (subrelstr ck) or not y in the carrier of (subrelstr ck) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr ck) )

assume that

A70: x in the carrier of (subrelstr ck) and

A71: y in the carrier of (subrelstr ck) and

ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

end;assume that

A70: x in the carrier of (subrelstr ck) and

A71: y in the carrier of (subrelstr ck) and

ex_inf_of {x,y},L ; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

per cases
( ( x = a & y = a ) or ( x = a & y = b ) or ( x = a & y = c ) or ( x = a & y = d ) or ( x = a & y = e ) or ( x = b & y = a ) or ( x = b & y = b ) or ( x = b & y = c ) or ( x = b & y = d ) or ( x = b & y = e ) or ( x = c & y = a ) or ( x = c & y = b ) or ( x = c & y = c ) or ( x = c & y = d ) or ( x = c & y = e ) or ( x = d & y = a ) or ( x = d & y = b ) or ( x = d & y = c ) or ( x = d & y = d ) or ( x = d & y = e ) or ( x = e & y = a ) or ( x = e & y = b ) or ( x = e & y = c ) or ( x = e & y = d ) or ( x = e & y = e ) )
by A68, A70, A71, ENUMSET1:def 3;

end;

suppose
( x = a & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" a
by YELLOW_0:40;

then inf {x,y} = a by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = a by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" b
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis: verum

suppose A72:
( x = a & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A73:
b <= d
by A64, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A73, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then inf {x,y} = a by A72, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= b by A59, YELLOW_0:25;

then a <= d by A73, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then inf {x,y} = a by A72, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A74:
( x = a & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A75:
c <= e
by A61, YELLOW_0:25;

a <= c by A60, YELLOW_0:25;

then a <= e by A75, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A74, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A60, YELLOW_0:25;

then a <= e by A75, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A74, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" b
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A59, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" b
by YELLOW_0:40;

then inf {x,y} = b by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = b by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis: verum

suppose A76:
( x = b & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A77:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then b <= e by A77, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then inf {x,y} = b by A76, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then b <= e by A77, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then inf {x,y} = b by A76, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = a "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A60, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" c
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A63, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" c
by YELLOW_0:40;

then inf {x,y} = c by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = c by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis: verum

suppose A78:
( x = d & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A79:
b <= d
by A64, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A79, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then inf {x,y} = a by A78, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= b by A59, YELLOW_0:25;

then a <= d by A79, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then inf {x,y} = a by A78, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = b "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A64, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" d
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A65, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = d )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = d "/\" d
by YELLOW_0:40;

then inf {x,y} = d by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then inf {x,y} = d by YELLOW_5:2;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = e )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = d "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A62, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A62, A68, ENUMSET1:def 3; :: thesis: verum

suppose A80:
( x = e & y = a )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A81:
c <= e
by A61, YELLOW_0:25;

a <= c by A60, YELLOW_0:25;

then a <= e by A81, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A80, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A60, YELLOW_0:25;

then a <= e by A81, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then inf {x,y} = a by A80, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A82:
( x = e & y = b )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

A83:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then b <= e by A83, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then inf {x,y} = b by A82, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then b <= e by A83, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then inf {x,y} = b by A82, YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = e & y = c )
; :: thesis: "/\" ({x,y},L) in the carrier of (subrelstr ck)

then
inf {x,y} = c "/\" e
by YELLOW_0:40;

hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "/\" ({x,y},L) in the carrier of (subrelstr ck) by A61, A68, ENUMSET1:def 3; :: thesis: verum

proof

then reconsider K = subrelstr ck as non empty full Sublattice of L by A69, YELLOW_0:def 15;
let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of (subrelstr ck) or not y in the carrier of (subrelstr ck) or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of (subrelstr ck) )

assume that

A84: x in the carrier of (subrelstr ck) and

A85: y in the carrier of (subrelstr ck) and

ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

end;assume that

A84: x in the carrier of (subrelstr ck) and

A85: y in the carrier of (subrelstr ck) and

ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

per cases
( ( x = a & y = a ) or ( x = a & y = b ) or ( x = a & y = c ) or ( x = a & y = d ) or ( x = a & y = e ) or ( x = b & y = a ) or ( x = b & y = b ) or ( x = b & y = c ) or ( x = b & y = d ) or ( x = b & y = e ) or ( x = c & y = a ) or ( x = c & y = b ) or ( x = c & y = c ) or ( x = c & y = d ) or ( x = c & y = e ) or ( x = d & y = a ) or ( x = d & y = b ) or ( x = d & y = c ) or ( x = d & y = d ) or ( x = d & y = e ) or ( x = e & y = a ) or ( x = e & y = b ) or ( x = e & y = c ) or ( x = e & y = d ) or ( x = e & y = e ) )
by A68, A84, A85, ENUMSET1:def 3;

end;

suppose
( x = a & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = a "\/" a
by YELLOW_0:41;

then sup {x,y} = a by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = a by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = b
by A59, Th5;

then sup {x,y} = b by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = a & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
x "\/" y = c
by A60, Th5;

then sup {x,y} = c by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A86:
( x = a & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A87:
b <= d
by A64, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A87, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then a "\/" d = d by Th5;

then sup {x,y} = d by A86, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= b by A59, YELLOW_0:25;

then a <= d by A87, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then a "\/" d = d by Th5;

then sup {x,y} = d by A86, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A88:
( x = a & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A89:
c <= e
by A61, YELLOW_0:25;

a <= c by A60, YELLOW_0:25;

then a <= e by A89, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A88, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A60, YELLOW_0:25;

then a <= e by A89, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A88, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A90:
( x = b & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

a "\/" b = b
by A59, Th5;

then sup {x,y} = b by A90, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by A90, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" b
by YELLOW_0:41;

then sup {x,y} = b by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = b by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = b & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" c
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis: verum

suppose A91:
( x = b & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

b "\/" d = d
by A64, Th5;

then sup {x,y} = d by A91, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by A91, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A92:
( x = b & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A93:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then b <= e by A93, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then b "\/" e = e by Th5;

then sup {x,y} = e by A92, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then b <= e by A93, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then b "\/" e = e by Th5;

then sup {x,y} = e by A92, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A94:
( x = c & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" a = c
by A60, Th5;

then sup {x,y} = c by A94, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by A94, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = b "\/" c
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A66, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" c
by YELLOW_0:41;

then sup {x,y} = c by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = c by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = c & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis: verum

suppose A95:
( x = c & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" e = e
by A61, Th5;

then sup {x,y} = e by A95, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A95, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A96:
( x = d & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A97:
b <= d
by A64, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A97, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then a "\/" d = d by Th5;

then sup {x,y} = d by A96, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= b by A59, YELLOW_0:25;

then a <= d by A97, ORDERS_2:3;

then a "/\" d = a by YELLOW_0:25;

then a "\/" d = d by Th5;

then sup {x,y} = d by A96, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A98:
( x = d & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

b "\/" d = d
by A64, Th5;

then sup {x,y} = d by A98, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by A98, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = c "\/" d
by YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis: verum

end;hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A67, A68, ENUMSET1:def 3; :: thesis: verum

suppose
( x = d & y = d )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

then
sup {x,y} = d "\/" d
by YELLOW_0:41;

then sup {x,y} = d by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = d by YELLOW_5:1;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A99:
( x = d & y = e )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

d "\/" e = e
by A62, Th5;

then sup {x,y} = e by A99, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A99, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A100:
( x = e & y = a )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A101:
c <= e
by A61, YELLOW_0:25;

a <= c by A60, YELLOW_0:25;

then a <= e by A101, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A100, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;a <= c by A60, YELLOW_0:25;

then a <= e by A101, ORDERS_2:3;

then a "/\" e = a by YELLOW_0:25;

then a "\/" e = e by Th5;

then sup {x,y} = e by A100, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A102:
( x = e & y = b )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

A103:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then b <= e by A103, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then b "\/" e = e by Th5;

then sup {x,y} = e by A102, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then b <= e by A103, ORDERS_2:3;

then b "/\" e = b by YELLOW_0:25;

then b "\/" e = e by Th5;

then sup {x,y} = e by A102, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

suppose A104:
( x = e & y = c )
; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr ck)

c "\/" e = e
by A61, Th5;

then sup {x,y} = e by A104, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

end;then sup {x,y} = e by A104, YELLOW_0:41;

hence "\/" ({x,y},L) in the carrier of (subrelstr ck) by A68, ENUMSET1:def 3; :: thesis: verum

take K ; :: thesis: N_5 ,K are_isomorphic

thus N_5 ,K are_isomorphic :: thesis: verum

proof

reconsider t = 3 as Element of N_5 by A1, ENUMSET1:def 3;

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

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

reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

defpred S_{1}[ object , object ] means for X being Element of N_5 st X = $1 holds

( ( X = z implies $2 = a ) & ( X = td implies $2 = b ) & ( X = dw implies $2 = c ) & ( X = tj implies $2 = d ) & ( X = t implies $2 = e ) );

ex y being object st

( y in ck & S_{1}[x,y] )

A123: for x being object st x in the carrier of N_5 holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A116);

reconsider f = f as Function of N_5,K by A68;

ck c= rng f

A157: for x, y being Element of N_5 holds

( x <= y iff f . x <= f . y )

f is V13() by A124;

hence f is isomorphic by A68, A156, A157, WAYBEL_0:66; :: thesis: verum

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

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

A106: now :: thesis: not dw = td

assume A107:
dw = td
; :: thesis: contradiction

2 in td by Th4, TARSKI:def 1;

hence contradiction by A107; :: thesis: verum

end;2 in td by Th4, TARSKI:def 1;

hence contradiction by A107; :: thesis: verum

A108: now :: thesis: not td = t

reconsider tj = 3 \ 1 as Element of N_5 by A1, ENUMSET1:def 3;assume A109:
td = t
; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A109, CARD_1:51, ENUMSET1:def 1; :: thesis: verum

end;not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A109, CARD_1:51, ENUMSET1:def 1; :: thesis: verum

reconsider z = 0 as Element of N_5 by A1, ENUMSET1:def 3;

defpred S

( ( X = z implies $2 = a ) & ( X = td implies $2 = b ) & ( X = dw implies $2 = c ) & ( X = tj implies $2 = d ) & ( X = t implies $2 = e ) );

A110: now :: thesis: not tj = dw

assume A111:
tj = dw
; :: thesis: contradiction

2 in tj by Th3, TARSKI:def 2;

hence contradiction by A111; :: thesis: verum

end;2 in tj by Th3, TARSKI:def 2;

hence contradiction by A111; :: thesis: verum

A112: now :: thesis: not tj = t

assume A113:
tj = t
; :: thesis: contradiction

not 0 in tj by Th3, TARSKI:def 2;

hence contradiction by A113, CARD_1:51, ENUMSET1:def 1; :: thesis: verum

end;not 0 in tj by Th3, TARSKI:def 2;

hence contradiction by A113, CARD_1:51, ENUMSET1:def 1; :: thesis: verum

A114: now :: thesis: not tj = td

A116:
for x being object st x in the carrier of N_5 holds assume A115:
tj = td
; :: thesis: contradiction

not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A115, Th3, TARSKI:def 2; :: thesis: verum

end;not 1 in td by Th4, TARSKI:def 1;

hence contradiction by A115, Th3, TARSKI:def 2; :: thesis: verum

ex y being object st

( y in ck & S

proof

consider f being Function of the carrier of N_5,ck such that
let x be object ; :: thesis: ( x in the carrier of N_5 implies ex y being object st

( y in ck & S_{1}[x,y] ) )

assume A117: x in the carrier of N_5 ; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

end;( y in ck & S

assume A117: x in the carrier of N_5 ; :: thesis: ex y being object st

( y in ck & S

per cases
( x = 0 or x = 3 \ 1 or x = 2 or x = 3 \ 2 or x = 3 )
by A1, A117, ENUMSET1:def 3;

end;

suppose A118:
x = 0
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = a; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A118, Th3, Th4; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A118, Th3, Th4; :: thesis: verum

suppose A119:
x = 3 \ 1
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = d; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A114, A112, A119, Th3; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A114, A112, A119, Th3; :: thesis: verum

suppose A120:
x = 2
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = c; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A106, A120; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A110, A106, A120; :: thesis: verum

suppose A121:
x = 3 \ 2
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = b; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A114, A106, A108, A121, Th4; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A114, A106, A108, A121, Th4; :: thesis: verum

suppose A122:
x = 3
; :: thesis: ex y being object st

( y in ck & S_{1}[x,y] )

( y in ck & S

take y = e; :: thesis: ( y in ck & S_{1}[x,y] )

thus y in ck by ENUMSET1:def 3; :: thesis: S_{1}[x,y]

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A112, A108, A122; :: thesis: verum

end;thus y in ck by ENUMSET1:def 3; :: thesis: S

let X be Element of N_5; :: thesis: ( 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 ) ) )

thus ( X = x implies ( ( X = z implies y = a ) & ( X = td implies y = b ) & ( X = dw implies y = c ) & ( X = tj implies y = d ) & ( X = t implies y = e ) ) ) by A112, A108, A122; :: thesis: verum

A123: for x being object st x in the carrier of N_5 holds

S

reconsider f = f as Function of N_5,K by A68;

A124: now :: thesis: for x, y being Element of N_5 st f . x = f . y holds

x = y

A146:
rng f c= ck
x = y

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

assume A125: f . x = f . y ; :: thesis: x = y

thus x = y :: thesis: verum

end;assume A125: f . x = f . y ; :: thesis: x = y

thus x = y :: thesis: verum

proof
end;

per cases
( ( x = z & y = z ) or ( x = tj & y = tj ) or ( x = td & y = td ) or ( x = dw & y = dw ) or ( x = t & y = t ) or ( x = z & y = tj ) or ( x = z & y = dw ) or ( x = z & y = td ) or ( x = z & y = t ) or ( x = tj & y = z ) or ( x = tj & y = dw ) or ( x = tj & y = td ) or ( x = tj & y = t ) or ( x = dw & y = z ) or ( x = dw & y = tj ) or ( x = dw & y = td ) or ( x = dw & y = t ) or ( x = td & y = z ) or ( x = td & y = tj ) or ( x = td & y = dw ) or ( x = td & y = t ) or ( x = t & y = z ) or ( x = t & y = tj ) or ( x = t & y = dw ) or ( x = t & y = td ) )
by A1, ENUMSET1:def 3;

end;

proof

A149:
dom f = the carrier of N_5
by FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in ck )

assume y in rng f ; :: thesis: y in ck

then consider x being object such that

A147: x in dom f and

A148: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of N_5 by A147;

( 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 A123, A148;

hence y in ck by ENUMSET1:def 3; :: thesis: verum

end;assume y in rng f ; :: thesis: y in ck

then consider x being object such that

A147: x in dom f and

A148: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of N_5 by A147;

( 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 A123, A148;

hence y in ck by ENUMSET1:def 3; :: thesis: verum

ck c= rng f

proof

then A156:
rng f = ck
by A146;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ck or y in rng f )

assume A150: y in ck ; :: thesis: y in rng f

end;assume A150: y in ck ; :: thesis: y in rng f

A157: for x, y being Element of N_5 holds

( x <= y iff f . x <= f . y )

proof

take
f
; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
let x, y be Element of N_5; :: thesis: ( x <= y iff f . x <= f . y )

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

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

proof

thus
( f . x <= f . y implies x <= y )
:: thesis: verum
assume A158:
x <= y
; :: thesis: f . x <= f . y

end;per cases
( ( x = z & y = z ) or ( x = z & y = td ) or ( x = z & y = dw ) or ( x = z & y = tj ) or ( x = z & y = t ) or ( x = td & y = z ) or ( x = td & y = td ) or ( x = td & y = dw ) or ( x = td & y = z ) or ( x = td & y = tj ) or ( x = td & y = t ) or ( x = dw & y = z ) or ( x = dw & y = td ) or ( x = dw & y = dw ) or ( x = dw & y = tj ) or ( x = dw & y = t ) or ( x = tj & y = z ) or ( x = tj & y = td ) or ( x = tj & y = dw ) or ( x = tj & y = tj ) or ( x = tj & y = t ) or ( x = t & y = z ) or ( x = t & y = td ) or ( x = t & y = dw ) or ( x = t & y = tj ) or ( x = t & y = t ) )
by A1, ENUMSET1:def 3;

end;

suppose A159:
( x = z & y = td )
; :: thesis: f . x <= f . y

then A160:
f . y = b
by A123;

A161: a <= b by A59, YELLOW_0:25;

f . x = a by A123, A159;

hence f . x <= f . y by A160, A161, YELLOW_0:60; :: thesis: verum

end;A161: a <= b by A59, YELLOW_0:25;

f . x = a by A123, A159;

hence f . x <= f . y by A160, A161, YELLOW_0:60; :: thesis: verum

suppose A162:
( x = z & y = dw )
; :: thesis: f . x <= f . y

then A163:
f . y = c
by A123;

A164: a <= c by A60, YELLOW_0:25;

f . x = a by A123, A162;

hence f . x <= f . y by A163, A164, YELLOW_0:60; :: thesis: verum

end;A164: a <= c by A60, YELLOW_0:25;

f . x = a by A123, A162;

hence f . x <= f . y by A163, A164, YELLOW_0:60; :: thesis: verum

suppose A165:
( x = z & y = tj )
; :: thesis: f . x <= f . y

A166:
b <= d
by A64, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then A167: a <= d by A166, ORDERS_2:3;

A168: f . y = d by A123, A165;

f . x = a by A123, A165;

hence f . x <= f . y by A168, A167, YELLOW_0:60; :: thesis: verum

end;a <= b by A59, YELLOW_0:25;

then A167: a <= d by A166, ORDERS_2:3;

A168: f . y = d by A123, A165;

f . x = a by A123, A165;

hence f . x <= f . y by A168, A167, YELLOW_0:60; :: thesis: verum

suppose A169:
( x = z & y = t )
; :: thesis: f . x <= f . y

A170:
c <= e
by A61, YELLOW_0:25;

a <= c by A60, YELLOW_0:25;

then A171: a <= e by A170, ORDERS_2:3;

A172: f . y = e by A123, A169;

f . x = a by A123, A169;

hence f . x <= f . y by A172, A171, YELLOW_0:60; :: thesis: verum

end;a <= c by A60, YELLOW_0:25;

then A171: a <= e by A170, ORDERS_2:3;

A172: f . y = e by A123, A169;

f . x = a by A123, A169;

hence f . x <= f . y by A172, A171, YELLOW_0:60; :: thesis: verum

suppose A173:
( x = td & y = dw )
; :: thesis: f . x <= f . y

A174:
not 2 in dw
;

2 in td by Th4, TARSKI:def 1;

then not td c= dw by A174;

hence f . x <= f . y by A158, A173, YELLOW_1:3; :: thesis: verum

end;2 in td by Th4, TARSKI:def 1;

then not td c= dw by A174;

hence f . x <= f . y by A158, A173, YELLOW_1:3; :: thesis: verum

suppose A175:
( x = td & y = tj )
; :: thesis: f . x <= f . y

then A176:
f . y = d
by A123;

A177: b <= d by A64, YELLOW_0:25;

f . x = b by A123, A175;

hence f . x <= f . y by A176, A177, YELLOW_0:60; :: thesis: verum

end;A177: b <= d by A64, YELLOW_0:25;

f . x = b by A123, A175;

hence f . x <= f . y by A176, A177, YELLOW_0:60; :: thesis: verum

suppose A178:
( x = td & y = t )
; :: thesis: f . x <= f . y

A179:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then A180: b <= e by A179, ORDERS_2:3;

A181: f . y = e by A123, A178;

f . x = b by A123, A178;

hence f . x <= f . y by A181, A180, YELLOW_0:60; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then A180: b <= e by A179, ORDERS_2:3;

A181: f . y = e by A123, A178;

f . x = b by A123, A178;

hence f . x <= f . y by A181, A180, YELLOW_0:60; :: thesis: verum

suppose A182:
( x = dw & y = td )
; :: thesis: f . x <= f . y

0 in dw
by CARD_1:50, TARSKI:def 2;

then not dw c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A182, YELLOW_1:3; :: thesis: verum

end;then not dw c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A182, YELLOW_1:3; :: thesis: verum

suppose A183:
( x = dw & y = tj )
; :: thesis: f . x <= f . y

0 in dw
by CARD_1:50, TARSKI:def 2;

then not dw c= tj by Th3, TARSKI:def 2;

hence f . x <= f . y by A158, A183, YELLOW_1:3; :: thesis: verum

end;then not dw c= tj by Th3, TARSKI:def 2;

hence f . x <= f . y by A158, A183, YELLOW_1:3; :: thesis: verum

suppose A184:
( x = dw & y = t )
; :: thesis: f . x <= f . y

then A185:
f . y = e
by A123;

A186: c <= e by A61, YELLOW_0:25;

f . x = c by A123, A184;

hence f . x <= f . y by A185, A186, YELLOW_0:60; :: thesis: verum

end;A186: c <= e by A61, YELLOW_0:25;

f . x = c by A123, A184;

hence f . x <= f . y by A185, A186, YELLOW_0:60; :: thesis: verum

suppose A187:
( x = tj & y = td )
; :: thesis: f . x <= f . y

1 in tj
by Th3, TARSKI:def 2;

then not tj c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A187, YELLOW_1:3; :: thesis: verum

end;then not tj c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A187, YELLOW_1:3; :: thesis: verum

suppose A188:
( x = tj & y = dw )
; :: thesis: f . x <= f . y

A189:
not 2 in dw
;

2 in tj by Th3, TARSKI:def 2;

then not tj c= dw by A189;

hence f . x <= f . y by A158, A188, YELLOW_1:3; :: thesis: verum

end;2 in tj by Th3, TARSKI:def 2;

then not tj c= dw by A189;

hence f . x <= f . y by A158, A188, YELLOW_1:3; :: thesis: verum

suppose A190:
( x = tj & y = t )
; :: thesis: f . x <= f . y

then A191:
f . y = e
by A123;

A192: d <= e by A62, YELLOW_0:25;

f . x = d by A123, A190;

hence f . x <= f . y by A191, A192, YELLOW_0:60; :: thesis: verum

end;A192: d <= e by A62, YELLOW_0:25;

f . x = d by A123, A190;

hence f . x <= f . y by A191, A192, YELLOW_0:60; :: thesis: verum

suppose A193:
( x = t & y = td )
; :: thesis: f . x <= f . y

0 in t
by CARD_1:51, ENUMSET1:def 1;

then not t c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A193, YELLOW_1:3; :: thesis: verum

end;then not t c= td by Th4, TARSKI:def 1;

hence f . x <= f . y by A158, A193, YELLOW_1:3; :: thesis: verum

suppose A194:
( x = t & y = dw )
; :: thesis: f . x <= f . y

A195:
not 2 in dw
;

2 in t by CARD_1:51, ENUMSET1:def 1;

then not t c= dw by A195;

hence f . x <= f . y by A158, A194, YELLOW_1:3; :: thesis: verum

end;2 in t by CARD_1:51, ENUMSET1:def 1;

then not t c= dw by A195;

hence f . x <= f . y by A158, A194, YELLOW_1:3; :: thesis: verum

suppose A196:
( x = t & y = tj )
; :: thesis: f . x <= f . y

0 in t
by CARD_1:51, ENUMSET1:def 1;

then not t c= tj by Th3, TARSKI:def 2;

hence f . x <= f . y by A158, A196, YELLOW_1:3; :: thesis: verum

end;then not t c= tj by Th3, TARSKI:def 2;

hence f . x <= f . y by A158, A196, YELLOW_1:3; :: thesis: verum

proof

A197:
f . y in ck
by A149, A156, FUNCT_1:def 3;

A198: f . x in ck by A149, A156, FUNCT_1:def 3;

assume A199: f . x <= f . y ; :: thesis: x <= y

end;A198: f . x in ck by A149, A156, FUNCT_1:def 3;

assume A199: f . x <= f . y ; :: thesis: x <= y

per cases
( ( f . x = a & f . y = a ) or ( f . x = a & f . y = b ) or ( f . x = a & f . y = c ) or ( f . x = a & f . y = d ) or ( f . x = a & f . y = e ) or ( f . x = b & f . y = a ) or ( f . x = b & f . y = b ) or ( f . x = b & f . y = c ) or ( f . x = b & f . y = d ) or ( f . x = b & f . y = e ) or ( f . x = c & f . y = a ) or ( f . x = c & f . y = b ) or ( f . x = c & f . y = c ) or ( f . x = c & f . y = d ) or ( f . x = c & f . y = e ) or ( f . x = d & f . y = a ) or ( f . x = d & f . y = b ) or ( f . x = d & f . y = c ) or ( f . x = d & f . y = d ) or ( f . x = d & f . y = e ) or ( f . x = e & f . y = a ) or ( f . x = e & f . y = b ) or ( f . x = e & f . y = c ) or ( f . x = e & f . y = d ) or ( f . x = e & f . y = e ) )
by A198, A197, ENUMSET1:def 3;

end;

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

f . z = a
by A123;

then z = x by A124, A200;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A124, A200;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

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

f . z = a
by A123;

then z = x by A124, A201;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A124, A201;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

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

f . z = a
by A123;

then z = x by A124, A202;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A124, A202;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

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

f . z = a
by A123;

then z = x by A124, A203;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then z = x by A124, A203;

then x c= y ;

hence x <= y by YELLOW_1:3; :: thesis: verum

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

f . tj = d
by A123;

then A205: y = tj by A124, A204;

f . td = b by A123;

then A206: x = td by A124, A204;

Segm 1 c= Segm 2 by NAT_1:39;

then x c= y by A206, A205, XBOOLE_1:34;

hence x <= y by YELLOW_1:3; :: thesis: verum

end;then A205: y = tj by A124, A204;

f . td = b by A123;

then A206: x = td by A124, A204;

Segm 1 c= Segm 2 by NAT_1:39;

then x c= y by A206, A205, XBOOLE_1:34;

hence x <= y by YELLOW_1:3; :: thesis: verum

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

f . t = e
by A123;

then A208: t = y by A124, A207;

f . td = b by A123;

then td = x by A124, A207;

hence x <= y by A208, YELLOW_1:3; :: thesis: verum

end;then A208: t = y by A124, A207;

f . td = b by A123;

then td = x by A124, A207;

hence x <= y by A208, YELLOW_1:3; :: thesis: verum

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

A210:
dw c= t

then A211: t = y by A124, A209;

f . dw = c by A123;

then dw = x by A124, A209;

hence x <= y by A210, A211, YELLOW_1:3; :: thesis: verum

end;proof

f . t = e
by A123;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in dw or X in t )

assume X in dw ; :: thesis: X in t

then ( X = 0 or X = 1 ) by CARD_1:50, TARSKI:def 2;

hence X in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

end;assume X in dw ; :: thesis: X in t

then ( X = 0 or X = 1 ) by CARD_1:50, TARSKI:def 2;

hence X in t by CARD_1:51, ENUMSET1:def 1; :: thesis: verum

then A211: t = y by A124, A209;

f . dw = c by A123;

then dw = x by A124, A209;

hence x <= y by A210, A211, YELLOW_1:3; :: thesis: verum

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

A213:
a <= b
by A59, YELLOW_0:25;

d <= a by A199, A212, YELLOW_0:59;

then d <= b by A213, ORDERS_2:3;

hence x <= y by AAA, A64, YELLOW_0:25; :: thesis: verum

end;d <= a by A199, A212, YELLOW_0:59;

then d <= b by A213, ORDERS_2:3;

hence x <= y by AAA, A64, YELLOW_0:25; :: thesis: verum

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

f . t = e
by A123;

then A215: t = y by A124, A214;

f . tj = d by A123;

then tj = x by A124, A214;

hence x <= y by A215, YELLOW_1:3; :: thesis: verum

end;then A215: t = y by A124, A214;

f . tj = d by A123;

then tj = x by A124, A214;

hence x <= y by A215, YELLOW_1:3; :: thesis: verum

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

A217:
b <= d
by A64, YELLOW_0:25;

A218: d <= e by A62, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A217, ORDERS_2:3;

then A219: a <= e by A218, ORDERS_2:3;

e <= a by A199, A216, YELLOW_0:59;

hence x <= y by AAA, A219, ORDERS_2:2; :: thesis: verum

end;A218: d <= e by A62, YELLOW_0:25;

a <= b by A59, YELLOW_0:25;

then a <= d by A217, ORDERS_2:3;

then A219: a <= e by A218, ORDERS_2:3;

e <= a by A199, A216, YELLOW_0:59;

hence x <= y by AAA, A219, ORDERS_2:2; :: thesis: verum

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

A221:
d <= e
by A62, YELLOW_0:25;

b <= d by A64, YELLOW_0:25;

then A222: b <= e by A221, ORDERS_2:3;

e <= b by A199, A220, YELLOW_0:59;

hence x <= y by AAA, A222, ORDERS_2:2; :: thesis: verum

end;b <= d by A64, YELLOW_0:25;

then A222: b <= e by A221, ORDERS_2:3;

e <= b by A199, A220, YELLOW_0:59;

hence x <= y by AAA, A222, ORDERS_2:2; :: thesis: verum

f is V13() by A124;

hence f is isomorphic by A68, A156, A157, WAYBEL_0:66; :: thesis: verum