### The Mizar article:

### The Jonsson Theorem

**by****Jaroslaw Gryko**

- Received November 13, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: LATTICE5
- [ MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, ORDINAL1, CLASSES1, ORDINAL2, MCART_1, PRALG_1, TARSKI, FUNCT_6, HAHNBAN, ZFMISC_1, ORDERS_1, LATTICE3, MSUALG_5, EQREL_1, LATTICES, BOOLE, WAYBEL_0, BHSP_3, SETFAM_1, CANTOR_1, RELAT_2, PRE_TOPC, GROUP_6, YELLOW_0, FILTER_2, CAT_1, FINSEQ_1, MATRIX_2, FINSEQ_2, ARYTM_1, SQUARE_1, REALSET1, SGRAPH1, CARD_1, PARTFUN1, LATTICE5; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_6, NUMBERS, XCMPLX_0, XREAL_0, BINARITH, CANTOR_1, NAT_1, SETFAM_1, ORDINAL1, ORDINAL2, CARD_1, MCART_1, DOMAIN_1, PARTFUN1, PRALG_1, PRE_TOPC, STRUCT_0, ORDERS_1, EQREL_1, MSUALG_5, FINSEQ_1, FINSEQ_2, CLASSES1, CQC_SIM1, LATTICES, LATTICE3, BINOP_1, YELLOW_0, WAYBEL_0, YELLOW_2, ABIAN, FINSOP_1; constructors BINARITH, DOMAIN_1, RFUNCT_3, CANTOR_1, MSUALG_5, CQC_SIM1, BINOP_1, CLASSES1, WAYBEL_1, LATTICE3, ABIAN, FINSOP_1, MEMBERED; clusters SUBSET_1, RELSET_1, STRUCT_0, INT_1, YELLOW_0, YELLOW_1, CARD_1, ORDINAL1, PRALG_1, LATTICE3, ABIAN, GOBOARD4, ARYTM_3, LATTICES, MEMBERED, NUMBERS, ORDINAL2, PARTFUN1, EQREL_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, LATTICE3, PRALG_1, WAYBEL_0, XBOOLE_0; theorems EQREL_1, CQC_SIM1, CQC_THE1, BINARITH, RELAT_1, RELAT_2, FINSEQ_1, FINSEQ_2, MSUALG_5, MSUALG_7, ORDERS_1, TARSKI, ENUMSET1, ORDINAL1, ORDINAL2, ORDINAL3, WELLORD2, HAHNBAN, PARTFUN1, GRFUNC_1, FUNCT_6, EXTENS_1, MCART_1, FINSEQ_5, NAT_1, AXIOMS, REAL_1, INT_1, BINOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, FILTER_0, LATTICES, LATTICE3, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_5, WAYBEL_0, WAYBEL_1, WAYBEL_6, CANTOR_1, RELSET_1, CARD_1, CLASSES1, FINSEQ_3, SCMFSA_7, SETFAM_1, XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1; schemes DOMAIN_1, FUNCT_1, FUNCT_2, YELLOW_2, RELSET_1, RECDEF_1, ORDINAL1, ORDINAL2, NAT_1, FINSEQ_1, ZFREFLE1; begin :: Preliminaries scheme RecChoice{A() -> set,P[set,set,set]}: ex f being Function st dom f = NAT & f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] provided A1: for n being Nat for x being set ex y being set st P[n,x,y] proof defpred Q[set,set,set] means ex O2 being Ordinal st O2 = $3 & (for X being set, n being Nat st X c= Rank the_rank_of $2 ex Y being set st Y c= Rank O2 & P[n,X,Y]) & (for O being Ordinal st for X being set, n being Nat st X c= Rank the_rank_of $2 ex Y being set st Y c= Rank O & P[n,X,Y] holds O2 c= O); A2: for n being Nat for x being set ex y being set st Q[n,x,y] proof let n be Nat; let x be set; defpred Y[set,set] means for m being Nat ex y being set st $2 is Ordinal & y c= Rank the_rank_of $2 & P[m,$1,y]; A3: for x' being set st x' in bool Rank the_rank_of x ex o being set st Y[x',o] proof let x' be set; assume x' in bool Rank the_rank_of x; defpred X[set,set] means ex y being set st $2 is Ordinal & y c= Rank the_rank_of $2 & P[$1,x',y]; A4: for e being set st e in NAT ex u being set st X[e,u] proof let i be set; assume i in NAT; then reconsider i' = i as Nat; thus ex o being set, y being set st o is Ordinal & y c= Rank the_rank_of o & P[i,x',y] proof consider y being set such that A5: P[i',x',y] by A1; take o = the_rank_of y, y; thus o is Ordinal; the_rank_of the_rank_of y = the_rank_of y by CLASSES1:81; hence y c= Rank the_rank_of o by CLASSES1:73; thus P[i,x',y] by A5; end; end; consider h being Function such that A6: dom h = NAT and A7: for i being set st i in NAT holds X[i,h.i] from NonUniqFuncEx(A4); take o = sup rng h; thus for m being Nat ex y being set st o is Ordinal & y c= Rank the_rank_of o & P[m,x',y] proof let m be Nat; consider y being set such that A8: h.m is Ordinal and A9: y c= Rank the_rank_of (h.m) and A10: P[m,x',y] by A7; take y; thus o is Ordinal; h.m in rng h by A6,FUNCT_1:def 5; then h.m in sup rng h by A8,ORDINAL2:27; then A11: h.m c= o by ORDINAL1:def 2; reconsider O = h.m as Ordinal by A8; A12: Rank O c= Rank o by A11,CLASSES1:43; y c= Rank O by A9,CLASSES1:81; then y c= Rank o by A12,XBOOLE_1:1; hence y c= Rank the_rank_of o by CLASSES1:81; thus P[m,x',y] by A10; end; end; consider f being Function such that A13: dom f = bool Rank the_rank_of x and A14: for x' being set st x' in bool Rank the_rank_of x holds Y[x',f.x'] from NonUniqFuncEx(A3); defpred X[Ordinal] means for X being set, n being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank $1 & P[n,X,Y]; A15: ex O being Ordinal st X[O] proof take O2 = sup rng f; thus (for X being set, m being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank O2 & P[m,X,Y]) proof let X be set; let m be Nat; assume A16: X c= Rank the_rank_of x; then consider Y being set such that A17: f.X is Ordinal and A18: Y c= Rank the_rank_of (f.X) and A19: P[m,X,Y] by A14; take Y; f.X in rng f by A13,A16,FUNCT_1:def 5; then f.X in sup rng f by A17,ORDINAL2:27; then A20:f.X c= O2 by ORDINAL1:def 2; reconsider O = f.X as Ordinal by A17; A21:Rank O c= Rank O2 by A20,CLASSES1:43; the_rank_of O = O by CLASSES1:81; hence Y c= Rank O2 by A18,A21,XBOOLE_1:1; thus P[m,X,Y] by A19; end; end; consider O2 being Ordinal such that A22: X[O2] & (for O being Ordinal st X[O] holds O2 c= O) from Ordinal_Min(A15); take O2; thus Q[n,x,O2] by A22; end; A23: for n being Nat for x,y1,y2 being set st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 proof let n be Nat; let x,y1,y2 be set; assume that A24: Q[n,x,y1] and A25: Q[n,x,y2]; consider O1 being Ordinal such that A26: O1 = y1 and A27: for X being set, n being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank O1 & P[n,X,Y] and A28: for O being Ordinal st for X being set, n being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank O & P[n,X,Y] holds O1 c= O by A24; consider O2 being Ordinal such that A29: O2 = y2 and A30: for X being set, n being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank O2 & P[n,X,Y] and A31: for O being Ordinal st for X being set, n being Nat st X c= Rank the_rank_of x ex Y being set st Y c= Rank O & P[n,X,Y] holds O2 c= O by A25; A32: O1 c= O2 by A28,A30; O2 c= O1 by A27,A31; hence y1 = y2 by A26,A29,A32,XBOOLE_0:def 10; end; consider g being Function such that A33: dom g = NAT and A34: g.0 = the_rank_of A() and A35: for n being Element of NAT holds Q[n,g.n,g.(n+1)] from RecEx(A2,A23); set beta = sup rng g; defpred X[set,set] means ex i being Nat st i = $1`2 & P[$1`2,$1`1,$2`1] & $2`2 = i+1 & not ex y being set st P[$1`2,$1`1,y] & the_rank_of y in the_rank_of $2`1; A36: for x being set st x in [:Rank beta, NAT:] ex u being set st X[x,u] proof let x be set; assume x in [:Rank beta, NAT:]; then consider a,b being set such that A37: a in Rank beta and A38: b in NAT and A39: x = [a,b] by ZFMISC_1:def 2; reconsider b as Nat by A38; the_rank_of a in beta by A37,CLASSES1:74; then consider alfa being Ordinal such that A40: alfa in rng g and A41: the_rank_of a c= alfa by ORDINAL2:29; A42: a c= Rank alfa by A41,CLASSES1:73; consider k being set such that A43: k in dom g and A44: alfa = g.k by A40,FUNCT_1:def 5; reconsider k as Nat by A33,A43; A45: Q[k,alfa,g.(k+1)] by A35,A44; then reconsider O2 = g.(k+1) as Ordinal; A46: x`2 = b & x`1 = a by A39,MCART_1:7; defpred X[Ordinal] means ex y being set st y c= Rank $1 & P[x`2,x`1,y]; a c= Rank the_rank_of alfa by A42,CLASSES1:81; then ex y being set st y c= Rank O2 & P[x`2,x`1,y] by A45,A46; then A47: ex O being Ordinal st X[O]; consider O being Ordinal such that A48: X[O] and A49: for O' being Ordinal st X[O'] holds O c= O' from Ordinal_Min(A47); consider Y being set such that A50: Y c= Rank O and A51: P[b,a,Y] by A46,A48; take u = [Y,b+1], i = b; thus i = x`2 by A39,MCART_1:7; thus P[x`2,x`1,u`1] by A46,A51,MCART_1:7; thus u`2 = i+1 by MCART_1:7; given y being set such that A52: P[x`2,x`1,y] and A53: the_rank_of y in the_rank_of u`1; A54: the_rank_of y in the_rank_of Y by A53,MCART_1:7; A55: the_rank_of Y c= O by A50,CLASSES1:73; y c= Rank the_rank_of y by CLASSES1:def 8; then O c= the_rank_of y by A49,A52; hence contradiction by A54,A55,ORDINAL1:7; end; consider F being Function such that dom F = [:Rank beta, NAT:] and A56: for x being set st x in [:Rank beta, NAT:] holds X[x,F.x] from NonUniqFuncEx(A36); deffunc U(Nat,set) = (F.[$2,$1])`1; consider f being Function such that A57: dom f = NAT and A58: f.0 = A() and A59: for n being Element of NAT holds f.(n+1) = U(n,f.n) from LambdaRecEx; take f; thus dom f = NAT by A57; thus f.0 = A() by A58; defpred X[Nat] means the_rank_of (f.$1) in sup rng g; g.0 in rng g by A33,FUNCT_1:def 5; then A60: X[0] by A34,A58,ORDINAL2:27; A61: for n being Element of NAT st X[n] holds X[n+1] proof let n be Element of NAT; assume A62: the_rank_of (f.n) in sup rng g; then f.n in Rank sup rng g by CLASSES1:74; then A63: [f.n,n] in [:Rank beta, NAT:] by ZFMISC_1:106; [f.n,n]`1 = f.n & [f.n,n]`2 = n by MCART_1:7; then consider i being Nat such that i = n and P[n,f.n,(F.[f.n,n])`1] and (F.[f.n,n])`2 = i+1 and A64: not ex y being set st P[n,f.n,y] & the_rank_of y in the_rank_of (F.[f.n,n])`1 by A56,A63; A65: f.(n+1) = (F.[f.n,n])`1 by A59; consider o1 being Ordinal such that A66: o1 in rng g and A67: the_rank_of (f.n) c= o1 by A62,ORDINAL2:29; consider m being set such that A68: m in dom g and A69: g.m = o1 by A66,FUNCT_1:def 5; reconsider m as Nat by A33,A68; consider o2 being Ordinal such that A70: o2 = g.(m+1) and A71: for X being set, n being Nat st X c= Rank the_rank_of (g.m) ex Y being set st Y c= Rank o2 & P[n,X,Y] and for o being Ordinal st for X being set, n being Nat st X c= Rank the_rank_of (g.m) ex Y being set st Y c= Rank o & P[n,X,Y] holds o2 c= o by A35; the_rank_of (f.n) c= the_rank_of (g.m) by A67,A69,CLASSES1:81; then f.n c= Rank the_rank_of (g.m) by CLASSES1:73; then consider YY being set such that A72: YY c= Rank o2 and A73: P[n,f.n,YY] by A71; not P[n,f.n,YY] or not the_rank_of YY in the_rank_of (F.[f.n,n])`1 by A64; then A74: the_rank_of (F.[f.n,n])`1 c= the_rank_of YY by A73,ORDINAL1:26; the_rank_of YY c= o2 by A72,CLASSES1:73; then A75: the_rank_of (f.(n+1)) c= o2 by A65,A74,XBOOLE_1:1; g.(m+1) in rng g by A33,FUNCT_1:def 5; then o2 in sup rng g by A70,ORDINAL2:27; hence the_rank_of (f.(n+1)) in sup rng g by A75,ORDINAL1:22; end; A76: for n being Element of NAT holds X[n] from Ind(A60,A61); A77: [A(),0]`1 = A() & [A(),0]`2 = 0 by MCART_1:7; the_rank_of A() in sup rng g by A58,A76; then A() in Rank sup rng g by CLASSES1:74; then [A(),0] in [:Rank beta, NAT:] by ZFMISC_1:106; then consider i being Nat such that i = [A(),0]`2 and A78: P[0,A(),(F.[A(),0])`1] and (F.[A(),0])`2 = i+1 and not ex y being set st P[0,A(),y] & the_rank_of y in the_rank_of (F.[A(),0])`1 by A56,A77; defpred X[Nat] means P[$1,f.$1,f.($1+1)]; A79: X[0] by A58,A59,A78; A80: for n being Element of NAT st X[n] holds X[n+1] proof let n be Element of NAT; assume P[n,f.n,f.(n+1)]; A81: [f.(n+1),n+1]`1 = f.(n+1) & [f.(n+1),n+1]`2 = n+1 by MCART_1:7; the_rank_of (f.(n+1)) in sup rng g by A76; then f.(n+1) in Rank sup rng g by CLASSES1:74; then [f.(n+1),n+1] in [:Rank beta, NAT:] by ZFMISC_1:106; then consider i being Nat such that i = n+1 and A82: P[n+1,f.(n+1),(F.[f.(n+1),n+1])`1] and (F.[f.(n+1),n+1])`2 = i+1 and not ex y being set st P[(n+1),f.(n+1),y] & the_rank_of y in the_rank_of (F.[f.(n+1),n+1])`1 by A56,A81; thus P[(n+1),f.(n+1),f.((n+1)+1)] by A59,A82; end; thus for n being Element of NAT holds X[n] from Ind(A79,A80); end; theorem Th1: for f being Function, F being Function-yielding Function st f = union rng F holds dom f = union rng doms F proof let f be Function; let F be Function-yielding Function; assume A1: f = union rng F; thus dom f c= union rng doms F proof let x be set; assume x in dom f; then [x,f.x] in union rng F by A1,FUNCT_1:def 4; then consider g being set such that A2: [x,f.x] in g & g in rng F by TARSKI:def 4; consider u being set such that A3: u in dom F & g = F.u by A2,FUNCT_1:def 5; x in dom (F.u) by A2,A3,FUNCT_1:8; then A4: x in (doms F).u by A3,FUNCT_6:31; u in dom doms F by A3,FUNCT_6:31; then (doms F).u in rng doms F by FUNCT_1:def 5; hence x in union rng doms F by A4,TARSKI:def 4; end; let x be set; assume x in union rng doms F; then consider A be set such that A5: x in A & A in rng doms F by TARSKI:def 4; consider u being set such that A6: u in dom doms F & A = (doms F).u by A5,FUNCT_1:def 5; A7: u in dom F by A6,EXTENS_1:3; then A8: F.u in rng F by FUNCT_1:def 5; consider g being Function such that A9: g = F.u; A = dom (F.u) by A6,A7,FUNCT_6:31; then [x,g.x] in F.u by A5,A9,FUNCT_1:def 4; then [x,g.x] in f by A1,A8,TARSKI:def 4; hence x in dom f by FUNCT_1:8; end; theorem Th2: for A,B being non empty set holds [:union A, union B:] = union { [:a,b:] where a is Element of A, b is Element of B : a in A & b in B } proof let A,B be non empty set; set Y = { [:a,b:] where a is Element of A, b is Element of B : a in A & b in B }; thus [:union A, union B:] c= union Y proof let z be set; assume A1: z in [:union A, union B:]; then consider x,y being set such that A2: z = [x,y] by ZFMISC_1:102; x in union A by A1,A2,ZFMISC_1:106; then consider a' being set such that A3: x in a' & a' in A by TARSKI:def 4; y in union B by A1,A2,ZFMISC_1:106; then consider b' being set such that A4: y in b' & b' in B by TARSKI:def 4; reconsider a' as Element of A by A3; reconsider b' as Element of B by A4; A5: z in [:a',b':] by A2,A3,A4,ZFMISC_1:def 2; [:a',b':] in Y; hence z in union Y by A5,TARSKI:def 4; end; let z be set; assume z in union Y; then consider e being set such that A6: z in e & e in Y by TARSKI:def 4; consider a' being Element of A, b' being Element of B such that A7: [:a',b':] = e & a' in A & b' in B by A6; consider x,y being set such that A8: x in a' & y in b' & z = [x,y] by A6,A7,ZFMISC_1:def 2; x in union A & y in union B by A8,TARSKI:def 4; hence z in [:union A, union B:] by A8,ZFMISC_1:def 2; end; theorem Th3: for A being non empty set st A is c=-linear holds [:union A, union A:] = union { [:a,a:] where a is Element of A : a in A } proof let A be non empty set; assume A1: A is c=-linear; set X = { [:a,a:] where a is Element of A : a in A }, Y = { [:a,b:] where a is Element of A, b is Element of A : a in A & b in A }; X c= Y proof let Z be set; assume Z in X; then consider a being Element of A such that A2: Z = [:a,a:] & a in A; thus Z in Y by A2; end; then A3: union X c= union Y by ZFMISC_1:95; union Y c= union X proof let Z be set; assume Z in union Y; then consider z being set such that A4: Z in z & z in Y by TARSKI:def 4; consider a,b being Element of A such that A5: z = [:a,b:] & a in A & b in A by A4; A6: a,b are_c=-comparable by A1,ORDINAL1:def 9; per cases by A6,XBOOLE_0:def 9; suppose a c= b; then [:a,b:] c= [:b,b:] by ZFMISC_1:118; then Z in [:b,b:] & [:b,b:] in X by A4,A5; hence Z in union X by TARSKI:def 4; suppose b c= a; then [:a,b:] c= [:a,a:] by ZFMISC_1:118; then Z in [:a,a:] & [:a,a:] in X by A4,A5; hence Z in union X by TARSKI:def 4; end; then union X = union Y by A3,XBOOLE_0:def 10; hence thesis by Th2; end; begin :: An equivalence lattice of a set reserve X for non empty set; definition let A be set; func EqRelLATT A -> Poset equals :Def1: LattPOSet EqRelLatt A; correctness; end; definition let A be set; cluster EqRelLATT A -> with_infima with_suprema; coherence proof LattPOSet EqRelLatt A is with_suprema with_infima; hence thesis by Def1; end; end; theorem Th4: for A, x being set holds x in the carrier of EqRelLATT A iff x is Equivalence_Relation of A proof let A, x be set; hereby assume x in the carrier of EqRelLATT A; then reconsider e = x as Element of LattPOSet EqRelLatt A by Def1; %e = e & %e is Element of EqRelLatt A by LATTICE3:def 4; then A1: x in the carrier of EqRelLatt A; the carrier of EqRelLatt A = {r where r is Relation of A,A : r is Equivalence_Relation of A} by MSUALG_5:def 2; then ex x' being Relation of A,A st x' = x & x' is Equivalence_Relation of A by A1; hence x is Equivalence_Relation of A; end; assume A2: x is Equivalence_Relation of A; the carrier of EqRelLatt A = {r where r is Relation of A,A : r is Equivalence_Relation of A} by MSUALG_5:def 2; then x in the carrier of EqRelLatt A by A2; then reconsider e = x as Element of EqRelLatt A; e% = e & e% is Element of LattPOSet EqRelLatt A by LATTICE3:def 3; then reconsider e as Element of EqRelLATT A by Def1; e in the carrier of EqRelLATT A; hence x in the carrier of EqRelLATT A; end; theorem Th5: for A being set, x,y being Element of EqRelLatt A holds x [= y iff x c= y proof let A be set, x,y be Element of EqRelLatt A; reconsider x' = x,y' = y as Equivalence_Relation of A by MSUALG_7:1; A1: x "/\" y = (the L_meet of EqRelLatt A).(x',y') by LATTICES:def 2 .= x' /\ y' by MSUALG_5:def 2; x' /\ y' = x' iff x' c= y' by XBOOLE_1:17,28; hence thesis by A1,LATTICES:21; end; theorem Th6: for A being set, a,b being Element of EqRelLATT A holds a <= b iff a c= b proof let A be set, a,b be Element of EqRelLATT A; set EL = EqRelLATT A, El = EqRelLatt A; a is Equivalence_Relation of A by Th4; then reconsider a' = a as Element of El by MSUALG_7:1; b is Equivalence_Relation of A by Th4; then reconsider b' = b as Element of El by MSUALG_7:1; A1: a'% = a & b'% = b by LATTICE3:def 3; A2: the InternalRel of EL = the InternalRel of LattPOSet El by Def1; thus a <= b implies a c= b proof assume a <= b; then [a,b] in the InternalRel of EL by ORDERS_1:def 9; then a'% <= b'% by A1,A2,ORDERS_1:def 9; then a' [= b' by LATTICE3:7; hence a c= b by Th5; end; thus a c= b implies a <= b proof assume a c= b; then a' [= b' by Th5; then a'% <= b'% by LATTICE3:7; hence a <= b by A1,Def1; end; end; theorem Th7: for L being Lattice, a,b being Element of LattPOSet L holds a "/\" b = %a "/\" %b proof let L be Lattice, a,b be Element of LattPOSet L; a = %a & b = %b by LATTICE3:def 4; then reconsider x = a, y = b as Element of L; set c = x "/\" y; A1:c [= x & c [= y by LATTICES:23; A2:c% = c & x% = x & y% = y & %(c%) = c% & %(x%) = x% & %(y%) = y% by LATTICE3:def 3,def 4; then reconsider c as Element of LattPOSet L; A3:c <= a & c <= b by A1,A2,LATTICE3:7; for d being Element of LattPOSet L st d <= a & d <= b holds d <= c proof let d be Element of LattPOSet L; assume A4: d <= a & d <= b; d = %d by LATTICE3:def 4; then reconsider z = d as Element of L; A5: z% = z & %(z%) = z% by LATTICE3:def 3,def 4; then z [= x & z [= y by A2,A4,LATTICE3:7; then z [= x "/\" y by FILTER_0:7; hence d <= c by A2,A5,LATTICE3:7; end; hence a "/\" b = %a "/\" %b by A2,A3,YELLOW_0:23; end; theorem Th8: for A being set, a,b being Element of EqRelLATT A holds a "/\" b = a /\ b proof let A be set, a,b be Element of EqRelLATT A; A1: now let x,y be Element of EqRelLatt A; reconsider e1 = x as Equivalence_Relation of A by MSUALG_7:1; reconsider e2 = y as Equivalence_Relation of A by MSUALG_7:1; thus x "/\" y = (the L_meet of EqRelLatt A).(e1,e2) by LATTICES:def 2 .= x /\ y by MSUALG_5:def 2; end; reconsider x = a as Element of LattPOSet EqRelLatt A by Def1; %x = x & %x is Element of EqRelLatt A by LATTICE3:def 4; then reconsider x as Element of EqRelLatt A; reconsider y = b as Element of LattPOSet EqRelLatt A by Def1; %y = y & %y is Element of EqRelLatt A by LATTICE3:def 4; then reconsider y as Element of EqRelLatt A; reconsider a1 = a,b1 = b as Element of LattPOSet EqRelLatt A by Def1; A2: x% = x & y% = y & %(x%) = x% & %(y%) = y% & %a1 = a1 & %b1 = b1 & (%a1)% = %a1 & (%b1)% = %b1 by LATTICE3:def 3,def 4; thus a "/\" b = a1 "/\" b1 by Def1 .= x "/\" y by A2,Th7 .= a /\ b by A1; end; theorem Th9: for L being Lattice, a,b being Element of LattPOSet L holds a "\/" b = %a "\/" %b proof let L be Lattice, a,b be Element of LattPOSet L; a = %a & b = %b by LATTICE3:def 4; then reconsider x = a, y = b as Element of L; set c = x "\/" y; A1: x [= c & y [= c by LATTICES:22; A2: c% = c & x% = x & y% = y & %(c%) = c% & %(x%) = x% & %(y%) = y% by LATTICE3:def 3,def 4; then reconsider c as Element of LattPOSet L; A3: a <= c & b <= c by A1,A2,LATTICE3:7; for d being Element of LattPOSet L st a <= d & b <= d holds c <= d proof let d be Element of LattPOSet L; assume A4: a <= d & b <= d; d = %d by LATTICE3:def 4; then reconsider z = d as Element of L; x% <= z% & y% <= z% by A2,A4,LATTICE3:def 3; then x [= z & y [= z by LATTICE3:7; then x "\/" y [= z by FILTER_0:6; then (x "\/" y)% <= z% by LATTICE3:7; hence c <= d by A2,LATTICE3:def 3; end; hence a "\/" b = %a "\/" %b by A2,A3,YELLOW_0:22; end; theorem Th10: for A being set, a,b being Element of EqRelLATT A for E1,E2 being Equivalence_Relation of A st a = E1 & b = E2 holds a "\/" b = E1 "\/" E2 proof let A be set, a,b be Element of EqRelLATT A, E1,E2 be Equivalence_Relation of A; assume that A1: a = E1 and A2: b = E2; reconsider x = a as Element of LattPOSet EqRelLatt A by Def1; %x = x & %x is Element of EqRelLatt A by LATTICE3:def 4; then reconsider x as Element of EqRelLatt A; reconsider y = b as Element of LattPOSet EqRelLatt A by Def1; %y = y & %y is Element of EqRelLatt A by LATTICE3:def 4; then reconsider y as Element of EqRelLatt A; reconsider a1 = a,b1 = b as Element of LattPOSet EqRelLatt A by Def1; A3: x% = x & y% = y & %(x%) = x% & %(y%) = y% & %a1 = a1 & %b1 = b1 & (%a1)% = %a1 & (%b1)% = %b1 by LATTICE3:def 3,def 4; thus a "\/" b = a1 "\/" b1 by Def1 .= x "\/" y by A3,Th9 .= (the L_join of EqRelLatt A).(x,y) by LATTICES:def 1 .= E1 "\/" E2 by A1,A2,MSUALG_5:def 2; end; definition let L be non empty RelStr; redefine attr L is complete means for X being Subset of L ex a being Element of L st a is_<=_than X & for b being Element of L st b is_<=_than X holds b <= a; compatibility proof hereby assume A1: L is complete; let X be Subset of L; set Y = { c where c is Element of L: c is_<=_than X }; consider p being Element of L such that A2: Y is_<=_than p and A3: for r being Element of L st Y is_<=_than r holds p <= r by A1,LATTICE3:def 12; take p; thus p is_<=_than X proof let q be Element of L; assume A4: q in X; Y is_<=_than q proof let s be Element of L; assume s in Y; then ex t being Element of L st s = t & t is_<=_than X; hence s <= q by A4,LATTICE3:def 8; end; hence p <= q by A3; end; let b be Element of L; assume b is_<=_than X; then b in Y; hence b <= p by A2,LATTICE3:def 9; end; assume A5: for X being Subset of L ex a being Element of L st a is_<=_than X & for b being Element of L st b is_<=_than X holds b <= a; let X be set; set Y = { c where c is Element of L: X is_<=_than c }; Y c= the carrier of L proof let x be set; assume x in Y; then ex c being Element of L st x = c & X is_<=_than c; hence x in the carrier of L; end; then consider p being Element of L such that A6: p is_<=_than Y and A7: for r being Element of L st r is_<=_than Y holds r <= p by A5; take p; thus X is_<=_than p proof let q be Element of L; assume A8: q in X; q is_<=_than Y proof let s be Element of L; assume s in Y; then ex t being Element of L st s = t & X is_<=_than t; hence q <= s by A8,LATTICE3:def 9; end; hence q <= p by A7; end; let r be Element of L; assume X is_<=_than r; then r in Y; hence p <= r by A6,LATTICE3:def 8; end; end; definition let A be set; cluster EqRelLATT A -> complete; coherence proof let X be Subset of EqRelLATT A; set B = X /\ the carrier of EqRelLATT A; B c= bool [:A,A:] proof let x be set; assume x in B; then x in the carrier of EqRelLATT A by XBOOLE_0:def 3; then x is Equivalence_Relation of A by Th4; hence x in bool [:A,A:]; end; then reconsider B as Subset-Family of [:A,A:] by SETFAM_1:def 7; consider b being Subset of [:A,A:] such that A1:b = Intersect(B); A2:for Y being set st Y in B holds Y is Equivalence_Relation of A proof let Y be set; assume Y in B; then Y in the carrier of EqRelLATT A by XBOOLE_0:def 3; hence Y is Equivalence_Relation of A by Th4; end; for x being set holds x in A implies [x,x] in b proof let x be set; assume A3:x in A; then A4:[x,x] in [:A,A:] by ZFMISC_1:def 2; for Y being set st Y in B holds [x,x] in Y proof let Y be set; assume Y in B; then Y is Equivalence_Relation of A by A2; hence [x,x] in Y by A3,EQREL_1:11; end; hence [x,x] in b by A1,A4,CANTOR_1:10; end; then A5:b is_reflexive_in A by RELAT_2:def 1; reconsider b as Relation of A by RELSET_1:def 1; A6: dom b = A & field b = A by A5,ORDERS_1:98; for x,y being set st x in A & y in A & [x,y] in b holds [y,x] in b proof let x,y be set; assume A8:x in A & y in A & [x,y] in b; then A9:[y,x] in [:A,A:] by ZFMISC_1:def 2; for Y being set st Y in B holds [y,x] in Y proof let Y be set; assume Y in B; then [x,y] in Y & Y is Equivalence_Relation of A by A1,A2,A8,CANTOR_1:10 ; hence [y,x] in Y by EQREL_1:12; end; hence [y,x] in b by A1,A9,CANTOR_1:10; end; then A10:b is_symmetric_in A by RELAT_2:def 3; for x,y,z being set holds x in A & y in A & z in A & [x,y] in b & [y,z] in b implies [x,z] in b proof let x,y,z be set; assume that A11:x in A & y in A & z in A and A12:[x,y] in b & [y,z] in b; A13:[x,z] in [:A,A:] by A11,ZFMISC_1:def 2; for Y being set st Y in B holds [x,z] in Y proof let Y be set; assume Y in B; then [x,y] in Y & [y,z] in Y & Y is Equivalence_Relation of A by A1,A2,A12,CANTOR_1:10; hence [x,z] in Y by EQREL_1:13; end; hence [x,z] in b by A1,A13,CANTOR_1:10; end; then b is_transitive_in A by RELAT_2:def 8; then reconsider b as Equivalence_Relation of A by A6,PARTFUN1:def 4,A10,RELAT_2:def 11,def 16; reconsider b as Element of EqRelLATT A by Th4; take b; now let a be Element of EqRelLATT A; assume A14: a in X /\ the carrier of EqRelLATT A; reconsider a' = a as Equivalence_Relation of A by Th4; reconsider b' = b as Equivalence_Relation of A; for x,y being set holds [x,y] in b' implies [x,y] in a' by A1,A14,CANTOR_1:10; then b' c= a' by RELAT_1:def 3; hence b <= a by Th6; end; then b is_<=_than X /\ the carrier of EqRelLATT A by LATTICE3:def 8; hence b is_<=_than X by YELLOW_0:5; let a be Element of EqRelLATT A; assume a is_<=_than X; then A15: a is_<=_than X /\ the carrier of EqRelLATT A by YELLOW_0:5; reconsider a' = a as Equivalence_Relation of A by Th4; A16: for d being Element of EqRelLATT A st d in B holds a' c= d proof let d be Element of EqRelLATT A; assume d in B; then a <= d by A15,LATTICE3:def 8; hence a' c= d by Th6; end; a' c= Intersect(B) proof let x be set; assume A17:x in a'; for Y being set st Y in B holds x in Y proof let Y be set; assume A18:Y in B; then Y in the carrier of EqRelLATT A by XBOOLE_0:def 3; then a' c= Y by A16,A18; hence x in Y by A17; end; hence x in Intersect(B) by A17,CANTOR_1:10; end; hence a <= b by A1,Th6; end; end; begin :: A type of a sublattice of equivalence lattice of a set definition let L1,L2 be LATTICE; cluster meet-preserving join-preserving map of L1,L2; existence proof consider z being Element of L2; deffunc U(set) = z; consider f being map of L1,L2 such that A1: for x being Element of L1 holds f.x = U(x) from LambdaMD; take f; for x,y being Element of L1 holds f.(x "/\" y) = f.x "/\" f.y proof let x,y be Element of L1; thus f.(x "/\" y) = z by A1 .= z "/\" z by YELLOW_5:2 .= f.x "/\" z by A1 .= f.x "/\" f.y by A1; end; hence f is meet-preserving by WAYBEL_6:1; for x,y being Element of L1 holds f.(x "\/" y) = f.x "\/" f.y proof let x,y be Element of L1; thus f.(x "\/" y) = z by A1 .= z "\/" z by YELLOW_5:1 .= f.x "\/" z by A1 .= f.x "\/" f.y by A1; end; hence f is join-preserving by WAYBEL_6:2; end; end; definition let L1,L2 be LATTICE; mode Homomorphism of L1,L2 is meet-preserving join-preserving map of L1,L2; end; definition let L be LATTICE; cluster meet-inheriting join-inheriting strict SubRelStr of L; existence proof consider a being Element of L; consider r be Relation of {a}; A1: {a} c= the carrier of L proof let x be set; assume x in {a}; then x = a by TARSKI:def 1; hence x in the carrier of L; end; r c= the InternalRel of L proof let z be set; assume z in r; then consider x,y be set such that A2: z = [x,y] & x in {a} & y in {a} by RELSET_1:6; x = a & y = a by A2,TARSKI:def 1; then z = [a,a] & a <= a by A2; hence z in the InternalRel of L by ORDERS_1:def 9; end; then reconsider S=RelStr(# {a}, r#) as strict SubRelStr of L by A1,YELLOW_0:def 13; take S; A3: for x,y being Element of L st x in {a} & y in {a} & ex_inf_of {x,y},L holds inf {x,y} in {a} proof let x,y be Element of L; assume x in {a} & y in {a} & ex_inf_of {x,y},L; then x = a & y = a by TARSKI:def 1; then inf {x,y} = a"/\"a by YELLOW_0:40 .= a by YELLOW_5:2; hence inf {x,y} in {a} by TARSKI:def 1; end; for x,y being Element of L st x in {a} & y in {a} & ex_sup_of {x,y},L holds sup {x,y} in {a} proof let x,y be Element of L; assume x in {a} & y in {a} & ex_sup_of {x,y},L; then x = a & y = a by TARSKI:def 1; then sup {x,y} = a"\/"a by YELLOW_0:41 .= a by YELLOW_5:1; hence sup {x,y} in {a} by TARSKI:def 1; end; hence thesis by A3,YELLOW_0:def 16,def 17; end; end; definition let L be non empty RelStr; mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L; end; definition let L1, L2 be LATTICE; let f be Homomorphism of L1,L2; redefine func Image f -> strict full Sublattice of L2; coherence proof set S = subrelstr rng f; A1: the carrier of S = rng f by YELLOW_0:def 15; A2: dom f = the carrier of L1 by FUNCT_2:def 1; for x,y being Element of L2 st x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L2 holds inf {x,y} in the carrier of S proof let x,y be Element of L2; assume A3: x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L2; then consider a being set such that A4: a in dom f & x = f.a by A1,FUNCT_1:def 5; consider b being set such that A5: b in dom f & y = f.b by A1,A3,FUNCT_1:def 5; reconsider a' = a, b' = b as Element of L1 by A4,A5; A6: f preserves_inf_of {a',b'} by WAYBEL_0:def 34; A7: ex_inf_of {a',b'},L1 by YELLOW_0:21; inf {x,y} = inf (f.:{a',b'}) by A4,A5,FUNCT_1:118 .= f.inf {a',b'} by A6,A7,WAYBEL_0:def 30; hence inf {x,y} in the carrier of S by A1,A2,FUNCT_1:def 5; end; then A8: S is meet-inheriting by YELLOW_0:def 16; for x,y being Element of L2 st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L2 holds sup {x,y} in the carrier of S proof let x,y be Element of L2; assume A9: x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L2; then consider a being set such that A10: a in dom f & x = f.a by A1,FUNCT_1:def 5; consider b being set such that A11: b in dom f & y = f.b by A1,A9,FUNCT_1:def 5; reconsider a' = a, b' = b as Element of L1 by A10,A11; A12: f preserves_sup_of {a',b'} by WAYBEL_0:def 35; A13: ex_sup_of {a',b'},L1 by YELLOW_0:20; sup {x,y} = sup (f.:{a',b'}) by A10,A11,FUNCT_1:118 .= f.sup {a',b'} by A12,A13,WAYBEL_0:def 31; hence sup {x,y} in the carrier of S by A1,A2,FUNCT_1:def 5; end; then S is join-inheriting by YELLOW_0:def 17; hence Image f is strict full Sublattice of L2 by A8,YELLOW_2:def 2; end; end; reserve e,e1,e2,e1',e2' for Equivalence_Relation of X, x,y,x',y' for set; definition let X; let f be non empty FinSequence of X; let x,y; let R1, R2 be Relation; pred x,y are_joint_by f,R1,R2 means :Def3: f.1 = x & f.(len f) = y & for i being Nat st 1 <= i & i < len f holds (i is odd implies [f.i,f.(i+1)] in R1) & (i is even implies [f.i,f.(i+1)] in R2); end; canceled; theorem Th12: for x being set, o being Nat, R1,R2 being Relation, f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds x,x are_joint_by f,R1,R2 proof let x be set, o be Nat, R1,R2 be Relation, f be non empty FinSequence of X; assume that A1:R1 is_reflexive_in X & R2 is_reflexive_in X and A2:f = o |-> x; A3: dom f = Seg(o) by A2,FINSEQ_2:68; then A4: 1 in Seg(o) & len f in Seg(o) by FINSEQ_5:6; then A5:f.1 = x by A2,FINSEQ_2:70; A6:f.(len f) = x by A2,A4,FINSEQ_2:70; for i being Nat st 1 <= i & i < len f holds (i is odd implies [f.i,f.(i+1)] in R1) & (i is even implies [f.i,f.(i+1)] in R2) proof let i be Nat; assume A7: 1 <= i & i < len f; A8: i is odd implies [f.i,f.(i+1)] in R1 proof assume i is odd; 1 <= i+1 & i+1 <= len f by A7,NAT_1:38; then i+1 in Seg(len f) by FINSEQ_1:3; then i+1 in Seg(o) by A2,FINSEQ_2:69; then A9: f.(i+1) = x by A2,FINSEQ_2:70; 1 <= i & i <= o by A2,A7,FINSEQ_2:69; then i in Seg(o) by FINSEQ_1:3; then A10: f.i = x by A2,FINSEQ_2:70; x in X by A3,A4,A5,FINSEQ_2:13; hence [f.i,f.(i+1)] in R1 by A1,A9,A10,RELAT_2:def 1; end; i is even implies [f.i,f.(i+1)] in R2 proof assume i is even; 1 <= i+1 & i+1 <= len f by A7,NAT_1:38; then i+1 in Seg(len f) by FINSEQ_1:3; then i+1 in Seg(o) by A2,FINSEQ_2:69; then A11: f.(i+1) = x by A2,FINSEQ_2:70; 1 <= i & i <= o by A2,A7,FINSEQ_2:69; then i in Seg(o) by FINSEQ_1:3; then A12: f.i = x by A2,FINSEQ_2:70; x in X by A3,A4,A5,FINSEQ_2:13; hence [f.i,f.(i+1)] in R2 by A1,A11,A12,RELAT_2:def 1; end; hence (i is odd implies [f.i,f.(i+1)] in R1) & (i is even implies [f.i,f.(i+1)] in R2) by A8; end; hence x,x are_joint_by f,R1,R2 by A5,A6,Def3; end; Lm1: now let i,n,m be Nat; assume 1 <= i & i < n+m; then 1 <= i & i < n or n = i & i < n+m or n < i & i < n+m by REAL_1:def 5; hence 1 <= i & i < n or n = i & i < n+m or n+1 <= i & i < n+m by NAT_1:38; end; canceled; theorem Th14: for x,y being set, R1,R2 being Relation, n,m being Nat st (n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st len f = n & x,y are_joint_by f,R1,R2) ex h being non empty FinSequence of X st len h = m & x,y are_joint_by h,R1,R2 proof let x,y be set, R1,R2 be Relation, n,m be Nat; assume that A1: n <= m and A2: R1 is_reflexive_in X & R2 is_reflexive_in X; given f being non empty FinSequence of X such that A3: len f = n & x,y are_joint_by f,R1,R2; A4: f.(len f) = y by A3,Def3; per cases by A1,REAL_1:def 5; suppose A5:n < m; reconsider i = m - n as Nat by A1,INT_1:18; A6: i > 0 by A5,SQUARE_1:11; len f in dom f by SCMFSA_7:12; then A7: y in rng f by A4,FUNCT_1:def 5; rng f c= X by FINSEQ_1:def 4; then reconsider y' = y as Element of X by A7; reconsider g = i |-> y' as FinSequence of X; len g <> 0 by A6,FINSEQ_2:69; then reconsider g as non empty FinSequence of X by FINSEQ_1:25; A8: 1 in dom g & len g in dom g by FINSEQ_5:6; A9: y,y are_joint_by g,R1,R2 by A2,Th12; reconsider h = f^g as non empty FinSequence of X; take h; thus len h = len f + len g by FINSEQ_1:35 .= n+(m-n) by A3,FINSEQ_2:69 .= n+m-n by XCMPLX_1:29 .= m+(n-n) by XCMPLX_1:29 .= m+0 by XCMPLX_1:14 .= m; A10: len g = m-n by FINSEQ_2:69; thus x,y are_joint_by h,R1,R2 proof rng f <> {} by RELAT_1:64; then 1 in dom f by FINSEQ_3:34; hence h.1 = f.1 by FINSEQ_1:def 7 .= x by A3,Def3; thus h.(len h) = h.(len f + len g) by FINSEQ_1:35 .= g.(len g) by A8,FINSEQ_1:def 7 .= y by A9,Def3; let j be Nat; assume A11: 1 <= j & j < len h; A12: dom f = Seg(len f) by FINSEQ_1:def 3; thus j is odd implies [h.j,h.(j+1)] in R1 proof assume A13: j is odd; per cases by A11,Lm1,FINSEQ_1:35; suppose A14: 1 <= j & j < len f; then 1 <= j+1 & j+1 <= len f by NAT_1:38; then j+1 in dom f by A12,FINSEQ_1:3; then A15: f.(j+1) = h.(j+1) by FINSEQ_1:def 7; j in dom f by A12,A14,FINSEQ_1:3; then f.j = h.j by FINSEQ_1:def 7; hence [h.j,h.(j+1)] in R1 by A3,A13,A14,A15,Def3; suppose A16: j = len f; then j in dom f by FINSEQ_5:6; then A17: h.j = y by A4,A16,FINSEQ_1:def 7; h.(j+1) = g.1 by A8,A16,FINSEQ_1:def 7 .= y by A9,Def3; hence [h.j,h.(j+1)] in R1 by A2,A17,RELAT_2:def 1; suppose A18: len f + 1 <= j & j < len f + len g; then A19: 1 <= j - len f by REAL_1:84; j - len f < len f + len g - len f by A18,REAL_1:54; then j - len f < len f - len f + len g by XCMPLX_1:29; then A20: j - len f < 0+len g by XCMPLX_1:14; 0 < j - len f by A19,AXIOMS:22; then 0 + len f < j -len f + len f by REAL_1:53; then len f < j + len f - len f by XCMPLX_1:29; then len f < j + (len f - len f) by XCMPLX_1:29; then A21: len f < j+0 by XCMPLX_1:14; then reconsider k = j - len f as Nat by INT_1:18; A22: 1 <= k+1 & k+1 <= len g by A19,A20,NAT_1:38; k in Seg (len g) by A19,A20,FINSEQ_1:3; then A23: g.k = y by A10,FINSEQ_2:70; k+1 in Seg (len g) by A22,FINSEQ_1:3; then A24: g.(k+1) = y by A10,FINSEQ_2:70; A25: j < j+1 by REAL_1:69; j+1 <= len f + len g by A18,NAT_1:38; then len f < j+1 & j+1 <= len h by A21,A25,AXIOMS:22,FINSEQ_1:35; then A26: h.(j+1) = g.(j+1-len f) by FINSEQ_1:37 .= g.(k+1) by XCMPLX_1:29; h.j = y by A18,A23,FINSEQ_1:36; hence [h.j,h.(j+1)] in R1 by A2,A24,A26,RELAT_2:def 1; end; assume A27: j is even; per cases by A11,Lm1,FINSEQ_1:35; suppose A28: 1 <= j & j < len f; then 1 <= j+1 & j+1 <= len f by NAT_1:38; then j+1 in dom f by A12,FINSEQ_1:3; then A29: f.(j+1) = h.(j+1) by FINSEQ_1:def 7; j in dom f by A12,A28,FINSEQ_1:3; then f.j = h.j by FINSEQ_1:def 7; hence [h.j,h.(j+1)] in R2 by A3,A27,A28,A29,Def3; suppose A30: j = len f; then j in dom f by FINSEQ_5:6; then A31: h.j = y by A4,A30,FINSEQ_1:def 7; h.(j+1) = g.1 by A8,A30,FINSEQ_1:def 7 .= y by A9,Def3; hence [h.j,h.(j+1)] in R2 by A2,A31,RELAT_2:def 1; suppose A32: len f + 1 <= j & j < len f + len g; then A33: 1 <= j - len f by REAL_1:84; j - len f < len f + len g - len f by A32,REAL_1:54; then j - len f < len f - len f + len g by XCMPLX_1:29; then A34: j - len f < 0+len g by XCMPLX_1:14; 0 < j - len f by A33,AXIOMS:22; then 0 + len f < j -len f + len f by REAL_1:53; then len f < j + len f - len f by XCMPLX_1:29; then len f < j + (len f - len f) by XCMPLX_1:29; then A35: len f < j+0 by XCMPLX_1:14; then reconsider k = j - len f as Nat by INT_1:18; A36: 1 <= k+1 & k+1 <= len g by A33,A34,NAT_1:38; k in Seg (len g) by A33,A34,FINSEQ_1:3; then A37: g.k = y by A10,FINSEQ_2:70; k+1 in Seg (len g) by A36,FINSEQ_1:3; then A38: g.(k+1) = y by A10,FINSEQ_2:70; A39: j < j+1 by REAL_1:69; j+1 <= len f + len g by A32,NAT_1:38; then len f < j+1 & j+1 <= len h by A35,A39,AXIOMS:22,FINSEQ_1:35; then A40: h.(j+1) = g.(j+1-len f) by FINSEQ_1:37 .= g.(k+1) by XCMPLX_1:29; h.j = y by A32,A37,FINSEQ_1:36; hence [h.j,h.(j+1)] in R2 by A2,A38,A40,RELAT_2:def 1; end; suppose n = m; hence thesis by A3; end; definition let X;let Y be Sublattice of EqRelLATT X; given e such that A1: e in the carrier of Y and A2: e <> id X; given o being Nat such that A3: for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = o & x,y are_joint_by F,e1,e2; func type_of Y -> Nat means :Def4: (for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = it+2 & x,y are_joint_by F,e1,e2)) & (ex e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & not (ex F being non empty FinSequence of X st len F = it+1 & x,y are_joint_by F,e1,e2)); existence proof defpred X[Nat] means for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = $1+2 & x,y are_joint_by F,e1,e2; set A = { n where n is Nat : X[n] }; A4: field e = X by EQREL_1:16; id X c= e by A4,RELAT_2:17; then not e c= id X by A2,XBOOLE_0:def 10; then consider x,y such that A5: [x,y] in e and A6: not [x,y] in id X by RELAT_1:def 3; A7: not x in X or x <> y by A6,RELAT_1:def 10; consider e1,e2 such that A8: e1 = e & e2 = e; A9: [x,y] in e1 "\/" e2 by A5,A8,EQREL_1:22; then consider F being non empty FinSequence of X such that A10: len F = o and A11: x,y are_joint_by F,e1,e2 by A1,A3,A8; A12: F.1 = x & F.(len F) = y & for i being Nat st 1 <= i & i < len F holds (i is odd implies [F.i,F.(i+1)] in e1) & (i is even implies [F.i,F.(i+1)] in e2) by A11,Def3; o >= 2 proof assume A13: not thesis; A14: 0 <= len F by NAT_1:18; len F < 1 + 1 by A10,A13; then len F <= 0 + 1 by NAT_1:38; then 0 = len F or len F = 1 by A14,NAT_1:27; hence contradiction by A4,A5,A7,A12,FINSEQ_1:25,RELAT_1:30; end; then consider o' being Nat such that A15: o = 2 + o' by NAT_1:28; consider k being Nat such that A16: k = o' & for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = k+2 & x,y are_joint_by F,e1,e2 by A3,A15; A17: k in A by A16; A is Subset of NAT from SubsetD; then reconsider A as non empty Subset of NAT by A17; set m = min A; m in A by CQC_SIM1:def 8; then consider m' being Nat such that A18: m' = m & for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = m'+2 & x,y are_joint_by F,e1,e2); ex e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & not (ex F being non empty FinSequence of X st len F = m+1 & x,y are_joint_by F,e1,e2) proof assume A19: not thesis; then consider F being non empty FinSequence of X such that A20: len F = m+1 & x,y are_joint_by F,e1,e2 by A1,A8,A9; A21: F.1 = x & F.(len F) = y by A20,Def3; len F >= 2 proof assume A22: not thesis; A23: 0 <= len F by NAT_1:18; len F < 1 + 1 by A22; then len F <= 0 + 1 by NAT_1:38; then 0 = len F or len F = 1 by A23,NAT_1:27; hence contradiction by A4,A5,A7,A21,FINSEQ_1:25,RELAT_1:30; end; then m + 1 >= 1 + 1 by A20; then A24: m >= 1 by REAL_1:53; then A25: m - 1 >= 0 by SQUARE_1:12; m < m + 1 by REAL_1:69; then m - 1 < m + 1 - 1 by REAL_1:54; then A26: m - 1 < m + (1 - 1) by XCMPLX_1:29; A27: m + 1 = (m + 1) + 1 - 1 by XCMPLX_1:26 .= m + (1 + 1) - 1 by XCMPLX_1:1 .= m - 1 + 2 by XCMPLX_1:29; m - 1 = m -' 1 by A24,SCMFSA_7:3; then A28: m -' 1 in A by A19,A27; m -' 1 < m by A25,A26,BINARITH:def 3; hence contradiction by A28,CQC_SIM1:def 8; end; hence thesis by A18; end; uniqueness proof let n1,n2 be Nat; assume A29: (for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = n1+2 & x,y are_joint_by F,e1,e2)); given e1',e2',x',y' such that A30: e1' in the carrier of Y & e2' in the carrier of Y & [x',y'] in e1' "\/" e2' and A31: not (ex F being non empty FinSequence of X st len F = n1+1 & x',y' are_joint_by F,e1',e2'); assume A32: (for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = n2+2 & x,y are_joint_by F,e1,e2)); given e1,e2,x,y such that A33: e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 and A34: not (ex F being non empty FinSequence of X st len F = n2+1 & x,y are_joint_by F,e1,e2); consider F1 being non empty FinSequence of X such that A35: len F1 = n1+2 & x,y are_joint_by F1,e1,e2 by A29,A33; consider F2 being non empty FinSequence of X such that A36: len F2 = n2+2 & x',y' are_joint_by F2,e1',e2' by A30,A32; A37: field e1 = X & field e2 = X by EQREL_1:16; A38: e1 is_reflexive_in X & e2 is_reflexive_in X by A37,RELAT_2:def 9; A39: field e1' = X & field e2' = X by EQREL_1:16; A40: e1' is_reflexive_in X & e2' is_reflexive_in X by A39,RELAT_2:def 9; assume A41:not thesis; per cases by A41,REAL_1:def 5; suppose n1 < n2; then n1+2 < n2+(1+1) by REAL_1:53; then n1+2 < (n2+1)+1 by XCMPLX_1:1; then n1+2 <= n2+1 by NAT_1:38; hence contradiction by A34,A35,A38,Th14; suppose n2 < n1; then n2+2 < n1+(1+1) by REAL_1:53; then n2+2 < (n1+1)+1 by XCMPLX_1:1; then n2+2 <= n1+1 by NAT_1:38; hence contradiction by A31,A36,A40,Th14; end; end; theorem Th15: for Y being Sublattice of EqRelLATT X, n being Nat st (ex e st e in the carrier of Y & e <> id X) & (for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = n+2 & x,y are_joint_by F,e1,e2)) holds type_of Y <= n proof let Y be Sublattice of EqRelLATT X, n be Nat; assume that A1: (ex e st e in the carrier of Y & e <> id X) and A2: for e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = n+2 & x,y are_joint_by F,e1,e2 and A3: n < type_of Y; n+1 <= type_of Y by A3,NAT_1:38; then consider m being Nat such that A4: type_of Y = (n+1)+m by NAT_1:28; n+1+m+1 = n+m+1+1 by XCMPLX_1:1 .= (n+m)+(1+1) by XCMPLX_1:1 .= n+m+2; then consider e1,e2,x,y such that A5: e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 and A6: not (ex F being non empty FinSequence of X st len F = (n+m)+2 & x,y are_joint_by F,e1,e2) by A1,A4,Def4; consider F1 being non empty FinSequence of X such that A7: len F1 = n+2 & x,y are_joint_by F1,e1,e2 by A2,A5; A8: field e1 = X & field e2 = X by EQREL_1:16; A9: e1 is_reflexive_in X & e2 is_reflexive_in X by A8,RELAT_2:def 9; n+2+m = (n+m)+2 by XCMPLX_1:1; then n+2 <= (n+m)+2 by NAT_1:29; hence contradiction by A6,A7,A9,Th14; end; begin :: A meet-representation of a lattice reserve A for non empty set, L for lower-bounded LATTICE; definition let A, L; mode BiFunction of A,L is Function of [:A,A:],the carrier of L; canceled; end; definition let A, L; let f be BiFunction of A,L;let x,y be Element of A; redefine func f.(x,y) -> Element of L; coherence proof reconsider xy = [x,y] as Element of [:A,A:]; f.xy is Element of L; hence thesis by BINOP_1:def 1; end; end; definition let A, L; let f be BiFunction of A,L; attr f is symmetric means :Def6: for x,y being Element of A holds f.(x,y) = f.(y,x); attr f is zeroed means :Def7: for x being Element of A holds f.(x,x) = Bottom L; attr f is u.t.i. means :Def8: for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z); end; :: f is u.t.i. means that f satisfies the triangle inequality definition let A, L; cluster symmetric zeroed u.t.i. BiFunction of A,L; existence proof deffunc U(Element of A,Element of A) = Bottom L; consider f being Function of [:A,A:],the carrier of L such that A1:for x,y being Element of A holds f.[x,y] = U(x,y) from Lambda2D; reconsider f as BiFunction of A,L; A2:for x,y being Element of A holds f.(x,y) = Bottom L proof let x,y be Element of A; reconsider x' = x as set; reconsider y' = y as set; Bottom L = f.[x,y] by A1 .= f.(x',y') by BINOP_1:def 1; hence thesis; end; for x,y being Element of A holds f.(x,y) = f.(y,x) proof let x,y be Element of A; thus f.(x,y) = Bottom L by A2 .= f.(y,x) by A2; end; then A3:f is symmetric by Def6; for x being Element of A holds f.(x,x) = Bottom L by A2; then A4:f is zeroed by Def7; for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z) proof let x,y,z be Element of A; A5: f.(x,y) = Bottom L & f.(y,z) = Bottom L by A2; f.(x,z) <= Bottom L by A2; hence thesis by A5,YELLOW_5:1; end; then f is u.t.i. by Def8; hence thesis by A3,A4; end; end; definition let A, L; mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L; end; definition let A, L; let d be distance_function of A,L; func alpha d -> map of L,EqRelLATT A means :Def9: for e being Element of L ex E being Equivalence_Relation of A st E = it.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e; existence proof defpred X[Element of L,Element of EqRelLATT A] means ex E being Equivalence_Relation of A st E = $2 & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= $1; A1:for e being Element of L ex r being Element of EqRelLATT A st X[e,r] proof let e be Element of L; defpred X[Element of A,Element of A] means d.($1,$2) <= e; consider E being Relation of A,A such that A2: for x,y being Element of A holds [x,y] in E iff X[x,y] from Rel_On_Dom_Ex; for x be set holds x in A implies [x,x] in E proof let x be set; assume x in A; then reconsider x' = x as Element of A; Bottom L <= e by YELLOW_0:44; then d.(x',x') <= e by Def7; hence [x,x] in E by A2; end; then E is_reflexive_in A by RELAT_2:def 1; then A3: dom E = A & field E = A by ORDERS_1:98; for x,y being set holds x in A & y in A & [x,y] in E implies [y,x] in E proof let x,y be set; assume that A5: x in A & y in A and A6: [x,y] in E; reconsider x' = x as Element of A by A5; reconsider y' = y as Element of A by A5; d.(x',y') <= e by A2,A6; then d.(y',x') <= e by Def6; hence [y,x] in E by A2; end; then A7: E is_symmetric_in A by RELAT_2:def 3; for x,y,z being set holds x in A & y in A & z in A & [x,y] in E & [y,z] in E implies [x,z] in E proof let x,y,z be set; assume that A8: x in A & y in A & z in A and A9: [x,y] in E & [y,z] in E; reconsider x' = x, y' = y, z' = z as Element of A by A8; d.(x',y') <= e & d.(y',z') <= e by A2,A9; then A10: d.(x',y') "\/" d.(y',z') <= e by YELLOW_0:22; d.(x',z') <= d.(x',y') "\/" d.(y',z') by Def8; then d.(x',z') <= e by A10,ORDERS_1:26; hence [x,z] in E by A2; end; then E is_transitive_in A by RELAT_2:def 8; then reconsider E as Equivalence_Relation of A by A3,PARTFUN1:def 4,A7,RELAT_2:def 11,def 16; reconsider E as Element of EqRelLATT A by Th4; consider r being Element of EqRelLATT A such that A11: r = E; thus thesis by A2,A11; end; consider f being map of L,EqRelLATT A such that A12: for e being Element of L holds X[e,f.e] from NonUniqExMD(A1); thus thesis by A12; end; uniqueness proof let f1,f2 be map of L,EqRelLATT A such that A13: for e being Element of L ex E being Equivalence_Relation of A st E = f1.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e and A14: for e being Element of L ex E being Equivalence_Relation of A st E = f2.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e; A15:for e being Element of L holds f1.e = f2.e proof let e be Element of L; consider E1 being Equivalence_Relation of A such that A16:E1 = f1.e & for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= e by A13; consider E2 being Equivalence_Relation of A such that A17:E2 = f2.e & for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= e by A14; A18:for x,y being Element of A holds [x,y] in E1 iff [x,y] in E2 proof let x,y be Element of A; [x,y] in E1 iff d.(x,y) <= e by A16; hence thesis by A17; end; for x,y being set holds [x,y] in E1 iff [x,y] in E2 proof let x,y be set; A19: field E1 = A & field E2 = A by EQREL_1:16; hereby assume A20:[x,y] in E1; then reconsider x' = x, y' = y as Element of A by A19,RELAT_1:30; [x',y'] in E2 by A18,A20; hence [x,y] in E2; end; assume A21:[x,y] in E2; then reconsider x' = x, y' = y as Element of A by A19,RELAT_1:30; [x',y'] in E1 by A18,A21; hence [x,y] in E1; end; hence thesis by A16,A17,RELAT_1:def 2; end; reconsider f1'=f1, f2'=f2 as Function of the carrier of L, the carrier of EqRelLATT A; for e be set st e in the carrier of L holds f1'.e = f2'.e by A15; hence f1 = f2 by FUNCT_2:18; end; end; theorem Th16: for d being distance_function of A,L holds alpha d is meet-preserving proof let d be distance_function of A,L; let a,b be Element of L; set f = alpha d; A1: ex_inf_of f.:{a,b},EqRelLATT A by YELLOW_0:17; A2: dom f = the carrier of L by FUNCT_2:def 1; consider E1 being Equivalence_Relation of A such that A3: E1 = f.a & for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def9; consider E2 being Equivalence_Relation of A such that A4: E2 = f.b & for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def9; consider E3 being Equivalence_Relation of A such that A5: E3 = f.(a "/\" b) & for x,y being Element of A holds [x,y] in E3 iff d.(x,y) <= a "/\" b by Def9; A6: for x,y being Element of A holds [x,y] in E1 /\ E2 iff [x,y] in E3 proof let x,y be Element of A; hereby assume [x,y] in E1 /\ E2; then [x,y] in E1 & [x,y] in E2 by XBOOLE_0:def 3; then d.(x,y) <= a & d.(x,y) <= b by A3,A4; then d.(x,y) <= a "/\" b by YELLOW_0:23; hence [x,y] in E3 by A5; end; assume [x,y] in E3; then A7: d.(x,y) <= a "/\" b by A5; a "/\" b <= a by YELLOW_0:23; then d.(x,y) <= a by A7,ORDERS_1:26; then A8: [x,y] in E1 by A3; a "/\" b <= b by YELLOW_0:23; then d.(x,y) <= b by A7,ORDERS_1:26; then [x,y] in E2 by A4; hence [x,y] in E1 /\ E2 by A8,XBOOLE_0:def 3; end; A9: for x,y being set holds [x,y] in E1 /\ E2 iff [x,y] in E3 proof let x,y be set; A10: field E3 = A by EQREL_1:16; field E1 /\ field E2 = A /\ field E2 by EQREL_1:16 .= A /\ A by EQREL_1:16 .= A; then A11: field (E1 /\ E2) c= A by RELAT_1:34; hereby assume A12:[x,y] in E1 /\ E2; then x in field (E1 /\ E2) & y in field (E1 /\ E2) by RELAT_1:30; then reconsider x' = x, y' = y as Element of A by A11; [x',y'] in E3 by A6,A12; hence [x,y] in E3; end; assume A13:[x,y] in E3; then reconsider x' = x, y' = y as Element of A by A10,RELAT_1:30; [x',y'] in E1 /\ E2 by A6,A13; hence [x,y] in E1 /\ E2; end; inf (f.:{a,b}) = inf {f.a,f.b} by A2,FUNCT_1:118 .= f.a "/\" f.b by YELLOW_0:40 .= E1 /\ E2 by A3,A4,Th8 .= f.(a "/\" b) by A5,A9,RELAT_1:def 2 .= f.inf {a,b} by YELLOW_0:40; hence f preserves_inf_of {a,b} by A1,WAYBEL_0:def 30; end; theorem Th17: for d being distance_function of A,L st d is onto holds alpha d is one-to-one proof let d be distance_function of A,L; assume d is onto; then A1: rng d = the carrier of L by FUNCT_2:def 3; set f = alpha d; for a,b being Element of L st f.a = f.b holds a = b proof let a,b be Element of L; assume A2:f.a = f.b; consider z1 be set such that A3: z1 in [:A,A:] & d.z1 = a by A1,FUNCT_2:17; consider x1,y1 being set such that A4: x1 in A & y1 in A & z1 = [x1,y1] by A3,ZFMISC_1:def 2; consider z2 be set such that A5: z2 in [:A,A:] & d.z2 = b by A1,FUNCT_2:17; consider x2,y2 being set such that A6: x2 in A & y2 in A & z2 = [x2,y2] by A5,ZFMISC_1:def 2; reconsider x1,y1 as Element of A by A4; reconsider x2,y2 as Element of A by A6; A7: d.(x1,y1) = a by A3,A4,BINOP_1:def 1; A8: d.(x2,y2) = b by A5,A6,BINOP_1:def 1; consider E1 being Equivalence_Relation of A such that A9:E1 = f.a & for x,y be Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def9; consider E2 being Equivalence_Relation of A such that A10:E2 = f.b & for x,y be Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def9; E1 = E2 & [x1,y1] in E1 by A2,A7,A9,A10; then A11: a <= b by A7,A10; E1 = E2 & [x2,y2] in E2 by A2,A8,A9,A10; then b <= a by A8,A9; hence a = b by A11,ORDERS_1:25; end; hence alpha d is one-to-one by WAYBEL_1:def 1; end; begin :: J\'onsson theorem definition let A be set; func new_set A equals :Def10: A \/ {{A}, {{A}}, {{{A}}} }; correctness; end; definition let A be set; cluster new_set A -> non empty; coherence proof {A} in {{A}, {{A}}, {{{A}}}} by ENUMSET1:14; then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; hence new_set A is non empty by Def10; end; end; definition let A,L; let d be BiFunction of A,L; let q be Element of [:A,A,the carrier of L,the carrier of L:]; func new_bi_fun(d,q) -> BiFunction of new_set A,L means :Def11: (for u,v being Element of A holds it.(u,v) = d.(u,v) ) & it.({A},{A}) = Bottom L & it.({{A}},{{A}}) = Bottom L & it.({{{A}}},{{{A}}}) = Bottom L & it.({{A}},{{{A}}}) = q`3 & it.({{{A}}},{{A}}) = q`3 & it.({A},{{A}}) = q`4 & it.({{A}},{A}) = q`4 & it.({A},{{{A}}}) = q`3"\/"q`4 & it.({{{A}}},{A}) = q`3"\/"q`4 & for u being Element of A holds (it.(u,{A}) = d.(u,q`1)"\/"q`3 & it.({A},u) = d.(u,q`1)"\/"q`3 & it.(u,{{A}}) = d.(u,q`1)"\/"q`3"\/"q`4 & it.({{A}},u) = d.(u,q`1)"\/"q`3"\/" q`4 & it.(u,{{{A}}}) = d.(u,q`2)"\/"q`4 & it.({{{A}}},u) = d.(u,q`2)"\/"q`4); existence proof set x = q`1, y = q`2; reconsider a = q`3, b = q`4 as Element of L; A1:{A} in new_set A & {{A}} in new_set A & {{{A}}} in new_set A proof {A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14; then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; hence {A} in new_set A by Def10; {{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14; then {{A}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; hence {{A}} in new_set A by Def10; {{{A}}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14; then {{{A}}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; hence {{{A}}} in new_set A by Def10; end; defpred X[Element of new_set A,Element of new_set A,Element of L] means ($1 in A & $2 in A implies $3 = d.($1,$2)) & ($1 = {{A}} & $2 = {{{A}}} or $2 = {{A}} & $1 = {{{A}}} implies $3 = a) & ($1 = {A} & $2 = {{A}} or $2 = {A} & $1 = {{A}} implies $3 = b) & ($1 = {A} & $2 = {{{A}}} or $2 = {A} & $1 = {{{A}}} implies $3 = a"\/"b) & (($1 = {A} or $1 = {{A}} or $1 = {{{A}}}) & $2 = $1 implies $3 = Bottom L) & ($1 in A & $2 = {A} implies ex p' being Element of A st p' = $1 & $3 = d.(p',x)"\/"a) & ($1 in A & $2 = {{A}} implies ex p' being Element of A st p' = $1 & $3 = d.(p',x)"\/"a"\/"b) & ($1 in A & $2 = {{{A}}} implies ex p' being Element of A st p' = $1 & $3 = d.(p',y)"\/"b) & ($2 in A & $1 = {A} implies ex q' being Element of A st q' = $2 & $3 = d.(q',x)"\/"a) & ($2 in A & $1 = {{A}} implies ex q' being Element of A st q' = $2 & $3 = d.(q',x)"\/"a"\/"b) & ($2 in A & $1 = {{{A}}} implies ex q' being Element of A st q' = $2 & $3 = d.(q',y)"\/"b); A2: for p,q being Element of new_set A ex r being Element of L st X[p,q,r] proof let p,q be Element of new_set A; p in new_set A & q in new_set A; then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10; then A3: (p in A or p in {{A},{{A}},{{{A}}}}) & (q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2; A4:{{A}} <> {{{A}}} proof assume {{A}} = {{{A}}}; then {{A}} in {{A}} by TARSKI:def 1; hence contradiction; end; A5: {A} <> {{{A}}} proof assume {A} = {{{A}}}; then {{A}} in {A} by TARSKI:def 1; hence contradiction by TARSKI:def 1; end; A6: not {A} in A by TARSKI:def 1; A7:not {{A}} in A proof assume A8: {{A}} in A; A in {A} & {A} in {{A}} by TARSKI:def 1; hence contradiction by A8,ORDINAL1:3; end; A9:not {{{A}}} in A proof assume A10: {{{A}}} in A; A in {A} & {A} in {{A}} & {{A}} in {{{A}}} by TARSKI:def 1; hence contradiction by A10,ORDINAL1:4; end; A11:(p = {A} or p = {{A}} or p = {{{A}}}) & p = q iff p = {A} & q = {A} or p = {{A}} & q = {{A}} or p = {{{A}}} & q = {{{A}}}; per cases by A3,A11,ENUMSET1:13; suppose p in A & q in A; then reconsider p'=p,q'=q as Element of A; take d.(p',q'); thus thesis by A6,A7,A9; suppose A12:p = {{A}} & q = {{{A}}} or q = {{A}} & p = {{{A}}}; take a; thus thesis by A4,A5,A7,A9,A12; suppose A13:p = {A} & q = {{A}} or q = {A} & p = {{A}}; take b; thus thesis by A4,A5,A7,A13,TARSKI:def 1; suppose A14:p = {A} & q = {{{A}}} or q = {A} & p = {{{A}}}; take a"\/"b; thus thesis by A4,A5,A9,A14,TARSKI:def 1; suppose A15: (p = {A} or p = {{A}} or p = {{{A}}}) & q = p; take Bottom L; thus thesis by A4,A5,A7,A9,A15,TARSKI:def 1; suppose A16:p in A & q = {A}; then reconsider p' = p as Element of A; take d.(p',x)"\/"a; thus thesis by A5,A7,A9,A16,TARSKI:def 1; suppose A17:p in A & q = {{A}}; then reconsider p' = p as Element of A; take d.(p',x)"\/"a"\/"b; thus thesis by A4,A7,A9,A17,TARSKI:def 1; suppose A18:p in A & q = {{{A}}}; then reconsider p' = p as Element of A; take d.(p',y)"\/"b; thus thesis by A4,A5,A7,A9,A18,TARSKI:def 1; suppose A19:q in A & p = {A}; then reconsider q' = q as Element of A; take d.(q',x)"\/"a; thus thesis by A5,A7,A9,A19,TARSKI:def 1; suppose A20:q in A & p = {{A}}; then reconsider q' = q as Element of A; take d.(q',x)"\/"a"\/"b; thus thesis by A4,A7,A9,A20,TARSKI:def 1; suppose A21:q in A & p = {{{A}}}; then reconsider q' = q as Element of A; take d.(q',y)"\/"b; thus thesis by A4,A5,A7,A9,A21,TARSKI:def 1; end; consider f being Function of [:new_set A,new_set A:],the carrier of L such that A22: for p,q being Element of new_set A holds X[p,q,f.[p,q]] from FuncEx2D(A2); reconsider f as BiFunction of new_set A,L; take f; A23: for u,v being Element of A holds f.(u,v) = d.(u,v) proof let u,v be Element of A; u in A \/ {{A}, {{A}}, {{{A}}}} & v in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; then reconsider u' = u, v' = v as Element of new_set A by Def10; thus f.(u,v) = f.[u',v'] by BINOP_1:def 1 .= d.(u,v) by A22; end; A24: f.({{A}},{{{A}}}) = f.[{{A}},{{{A}}}] by BINOP_1:def 1 .= a by A1,A22; A25:f.({{{A}}},{{A}}) = f.[{{{A}}},{{A}}] by BINOP_1:def 1 .= a by A1,A22; A26: f.({A},{{A}}) = f.[{A},{{A}}] by BINOP_1:def 1 .= b by A1,A22; A27:f.({{A}},{A}) = f.[{{A}},{A}] by BINOP_1:def 1 .= b by A1,A22; A28: f.({A},{{{A}}}) = f.[{A},{{{A}}}] by BINOP_1:def 1 .= a"\/"b by A1,A22; A29:f.({{{A}}},{A}) = f.[{{{A}}},{A}] by BINOP_1:def 1 .= a"\/"b by A1,A22; A30: f.({A},{A}) = f.[{A},{A}] by BINOP_1:def 1 .= Bottom L by A1,A22; A31: f.({{A}},{{A}}) = f.[{{A}},{{A}}] by BINOP_1:def 1 .= Bottom L by A1,A22; A32: f.({{{A}}},{{{A}}}) = f.[{{{A}}},{{{A}}}] by BINOP_1:def 1 .= Bottom L by A1,A22 ; A33:for u being Element of A holds (f.(u,{A}) = d.(u,x)"\/"a & f.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f.(u,{{{A}}}) = d.(u,y)"\/"b) proof let u be Element of A; u in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; then reconsider u' = u as Element of new_set A by Def10; consider u1 being Element of A such that A34: u1 = u' & f.[u',{A}] = d.(u1,x)"\/"a by A1,A22; thus f.(u,{A}) = d.(u,x)"\/"a by A34,BINOP_1:def 1; consider u2 being Element of A such that A35: u2 = u' & f.[u',{{A}}] = d.(u2,x)"\/"a"\/"b by A1,A22; thus f.(u,{{A}}) = d.(u,x)"\/"a"\/"b by A35,BINOP_1:def 1; consider u3 being Element of A such that A36: u3 = u' & f.[u',{{{A}}}] = d.(u3,y)"\/"b by A1,A22; thus f.(u,{{{A}}}) = d.(u,y)"\/"b by A36,BINOP_1:def 1; end; for u being Element of A holds (f.({A},u) = d.(u,x)"\/"a & f.({{A}},u) = d.(u,x)"\/"a"\/"b & f.({{{A}}},u) = d.(u,y)"\/"b) proof let u be Element of A; u in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; then reconsider u' = u as Element of new_set A by Def10; consider u1 being Element of A such that A37: u1 = u' & f.[{A},u'] = d.(u1,x)"\/"a by A1,A22; thus f.({A},u) = d.(u,x)"\/"a by A37,BINOP_1:def 1; consider u2 being Element of A such that A38: u2 = u' & f.[{{A}},u'] = d.(u2,x)"\/"a"\/"b by A1,A22; thus f.({{A}},u) = d.(u,x)"\/"a"\/"b by A38,BINOP_1:def 1; consider u3 being Element of A such that A39: u3 = u' & f.[{{{A}}},u'] = d.(u3,y)"\/"b by A1,A22; thus f.({{{A}}},u) = d.(u,y)"\/"b by A39,BINOP_1:def 1; end; hence thesis by A23,A24,A25,A26,A27,A28,A29,A30,A31,A32,A33; end; uniqueness proof set x = q`1, y = q`2, a = q`3, b = q`4; let f1,f2 be BiFunction of new_set A,L such that A40: (for u,v being Element of A holds f1.(u,v) = d.(u,v) ) & f1.({A},{A}) = Bottom L & f1.({{A}},{{A}}) = Bottom L & f1.({{{A}}},{{{A}}}) = Bottom L & f1.({{A}},{{{A}}}) = a & f1.({{{A}}},{{A}}) = a & f1.({A},{{A}}) = b & f1.({{A}},{A}) = b & f1.({A},{{{A}}}) = a"\/"b & f1.({{{A}}},{A}) = a"\/"b & for u being Element of A holds (f1.(u,{A}) = d.(u,x)"\/"a & f1.({A},u) = d.(u,x)"\/"a & f1.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f1.({{A}},u) = d.(u,x)"\/"a"\/"b & f1.(u,{{{A}}}) = d.(u,y)"\/"b & f1.({{{A}}},u) = d.(u,y)"\/"b) and A41: (for u,v being Element of A holds f2.(u,v) = d.(u,v) ) & f2.({A},{A}) = Bottom L & f2.({{A}},{{A}}) = Bottom L & f2.({{{A}}},{{{A}}}) = Bottom L & f2.({{A}},{{{A}}}) = a & f2.({{{A}}},{{A}}) = a & f2.({A},{{A}}) = b & f2.({{A}},{A}) = b & f2.({A},{{{A}}}) = a"\/"b & f2.({{{A}}},{A}) = a"\/"b & for u being Element of A holds (f2.(u,{A}) = d.(u,x)"\/"a & f2.({A},u) = d.(u,x)"\/"a & f2.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f2.({{A}},u) = d.(u,x)"\/"a"\/"b & f2.(u,{{{A}}}) = d.(u,y)"\/"b & f2.({{{A}}},u) = d.(u,y)"\/"b); now let p,q be Element of new_set A; p in new_set A & q in new_set A; then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10; then A42: (p in A or p in {{A},{{A}},{{{A}}}}) & (q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2; per cases by A42,ENUMSET1:13; suppose A43:p in A & q in A; hence f1.(p,q) = d.(p,q) by A40 .= f2.(p,q) by A41,A43; suppose A44:p in A & q = {A}; then reconsider p' = p as Element of A; thus f1.(p,q) = d.(p',x)"\/"a by A40,A44 .= f2.(p,q) by A41,A44; suppose A45:p in A & q = {{A}}; then reconsider p' = p as Element of A; thus f1.(p,q) = d.(p',x)"\/"a"\/"b by A40,A45 .= f2.(p,q) by A41,A45; suppose A46:p in A & q = {{{A}}}; then reconsider p' = p as Element of A; thus f1.(p,q) = d.(p',y)"\/"b by A40,A46 .= f2.(p,q) by A41,A46; suppose A47:p = {A} & q in A; then reconsider q' = q as Element of A; thus f1.(p,q) = d.(q',x)"\/"a by A40,A47 .= f2.(p,q) by A41,A47; suppose p = {A} & q = {A}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {A} & q = {{A}}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {A} & q = {{{A}}}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose A48:p = {{A}} & q in A; then reconsider q' = q as Element of A; thus f1.(p,q) = d.(q',x)"\/"a"\/"b by A40,A48 .= f2.(p,q) by A41,A48; suppose p = {{A}} & q = {A}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {{A}} & q = {{A}}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {{A}} & q = {{{A}}}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose A49:p = {{{A}}} & q in A; then reconsider q' = q as Element of A; thus f1.(p,q) = d.(q',y)"\/"b by A40,A49 .= f2.(p,q) by A41,A49; suppose p = {{{A}}} & q = {A}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {{{A}}} & q = {{A}}; hence f1.(p,q) = f2.(p,q) by A40,A41; suppose p = {{{A}}} & q = {{{A}}}; hence f1.(p,q) = f2.(p,q) by A40,A41; end; hence f1 = f2 by BINOP_1:2; end; end; theorem Th18: for d being BiFunction of A,L st d is zeroed for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun(d,q) is zeroed proof let d be BiFunction of A,L; assume A1: d is zeroed; let q be Element of [:A,A,the carrier of L,the carrier of L:]; set f = new_bi_fun(d,q); for u being Element of new_set A holds f.(u,u) = Bottom L proof let u be Element of new_set A; u in new_set A; then u in A \/ {{A},{{A}},{{{A}}}} by Def10; then A2:u in A or u in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 2; per cases by A2,ENUMSET1:13; suppose u in A; then reconsider u' = u as Element of A; thus f.(u,u) = d.(u',u') by Def11 .= Bottom L by A1,Def7; suppose u = {A} or u = {{A}} or u = {{{A}}}; hence f.(u,u) = Bottom L by Def11; end; hence thesis by Def7; end; theorem Th19: for d being BiFunction of A,L st d is symmetric for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun(d,q) is symmetric proof let d be BiFunction of A,L; assume A1: d is symmetric; let q be Element of [:A,A,the carrier of L,the carrier of L:]; set f = new_bi_fun(d,q), x = q`1, y = q`2, a = q`3, b = q`4; let p,q be Element of new_set A; p in new_set A & q in new_set A; then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10; then A2: (p in A or p in {{A},{{A}},{{{A}}}}) & (q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2; per cases by A2,ENUMSET1:13; suppose p in A & q in A; then reconsider p' = p, q' = q as Element of A; thus f.(p,q) = d.(p',q') by Def11 .= d.(q',p') by A1,Def6 .= f.(q,p) by Def11; suppose A3:p in A & q = {A}; then reconsider p' = p as Element of A; thus f.(p,q) = d.(p',x)"\/"a by A3,Def11 .= f.(q,p) by A3,Def11; suppose A4:p in A & q = {{A}}; then reconsider p' = p as Element of A; thus f.(p,q) = d.(p',x)"\/"a"\/"b by A4,Def11 .= f.(q,p) by A4,Def11; suppose A5:p in A & q = {{{A}}}; then reconsider p' = p as Element of A; thus f.(p,q) = d.(p',y)"\/"b by A5,Def11 .= f.(q,p) by A5,Def11; suppose A6:p = {A} & q in A; then reconsider q' = q as Element of A; thus f.(p,q) = d.(q',x)"\/"a by A6,Def11 .= f.(q,p) by A6,Def11; suppose p = {A} & q = {A}; hence f.(p,q) = f.(q,p); suppose A7:p = {A} & q = {{A}}; hence f.(p,q) = b by Def11 .= f.(q,p) by A7,Def11; suppose A8:p = {A} & q = {{{A}}}; hence f.(p,q) = a"\/"b by Def11 .= f.(q,p) by A8,Def11; suppose A9:p = {{A}} & q in A; then reconsider q' = q as Element of A; thus f.(p,q) = d.(q',x)"\/"a"\/"b by A9,Def11 .= f.(q,p) by A9,Def11; suppose A10:p = {{A}} & q = {A}; hence f.(p,q) = b by Def11 .= f.(q,p) by A10,Def11; suppose p = {{A}} & q = {{A}}; hence f.(p,q) = f.(q,p); suppose A11:p = {{A}} & q = {{{A}}}; hence f.(p,q) = a by Def11 .= f.(q,p) by A11,Def11; suppose A12:p = {{{A}}} & q in A; then reconsider q' = q as Element of A; thus f.(p,q) = d.(q',y)"\/"b by A12,Def11 .= f.(q,p) by A12,Def11; suppose A13:p = {{{A}}} & q = {A}; hence f.(p,q) = a"\/"b by Def11 .= f.(q,p) by A13,Def11; suppose A14:p = {{{A}}} & q = {{A}}; hence f.(p,q) = a by Def11 .= f.(q,p) by A14,Def11; suppose p = {{{A}}} & q = {{{A}}}; hence f.(p,q) = f.(q,p); end; theorem Th20: for d being BiFunction of A,L st d is symmetric & d is u.t.i. for q being Element of [:A,A,the carrier of L,the carrier of L:] st d.(q`1,q`2) <= q`3"\/"q`4 holds new_bi_fun(d,q) is u.t.i. proof let d be BiFunction of A,L; assume that A1: d is symmetric and A2: d is u.t.i.; let q be Element of [:A,A,the carrier of L,the carrier of L:]; assume A3: d.(q`1,q`2) <= q`3"\/"q`4; set x = q`1, y = q`2, f = new_bi_fun(d,q); reconsider B = {{A}, {{A}}, {{{A}}}} as non empty set by ENUMSET1:14; reconsider a = q`3,b = q`4 as Element of L; A4: for p,q,u being Element of new_set A st p in A & q in A & u in A holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume p in A & q in A & u in A; then reconsider p' = p, q' = q, u' = u as Element of A; A5:f.(p,u) = d.(p',u') by Def11; A6:f.(p,q) = d.(p',q') by Def11; f.(q,u) = d.(q',u') by Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A2,A5,A6,Def8; end; A7: for p,q,u being Element of new_set A st p in A & q in A & u in B holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A8: p in A & q in A & u in B; per cases by A8,ENUMSET1:13; suppose A9:p in A & q in A & u = {A}; then reconsider p' = p, q' = q as Element of A; A10:f.(p,u) = d.(p',x)"\/"a by A9,Def11; A11:f.(q,u) = d.(q',x)"\/"a by A9,Def11; A12:f.(p,q) = d.(p',q') by Def11; d.(p',x) <= d.(p',q') "\/" d.(q',x) by A2,Def8; then d.(p',x)"\/"a <= (d.(p',q') "\/" d.(q',x))"\/"a by WAYBEL_1:3; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A10,A11,A12,LATTICE3:14; suppose A13:p in A & q in A & u = {{A}}; then reconsider p' = p, q' = q as Element of A; A14:f.(p,u) = d.(p',x)"\/"a"\/"b by A13,Def11; A15:f.(q,u) = d.(q',x)"\/"a"\/"b by A13,Def11; A16:f.(p,q) = d.(p',q') by Def11; d.(p',x) <= d.(p',q') "\/" d.(q',x) by A2,Def8; then d.(p',x)"\/"a <= (d.(p',q') "\/" d.(q',x))"\/"a by WAYBEL_1:3; then (d.(p',x)"\/"a)"\/"b <= ((d.(p',q') "\/" d.(q',x))"\/"a)"\/" b by WAYBEL_1:3; then d.(p',x)"\/"a"\/"b <= (d.(p',q') "\/" (d.(q',x)"\/"a))"\/"b by LATTICE3 :14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A14,A15,A16,LATTICE3:14; suppose A17:p in A & q in A & u = {{{A}}}; then reconsider p' = p, q' = q as Element of A; A18:f.(p,u) = d.(p',y)"\/"b by A17,Def11; A19:f.(q,u) = d.(q',y)"\/"b by A17,Def11; A20:f.(p,q) = d.(p',q') by Def11; d.(p',y) <= d.(p',q') "\/" d.(q',y) by A2,Def8; then d.(p',y)"\/"b <= (d.(p',q') "\/" d.(q',y))"\/"b by WAYBEL_1:3; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A18,A19,A20,LATTICE3:14; end; A21: for p,q,u being Element of new_set A st p in A & q in B & u in A holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A22:p in A & q in B & u in A; per cases by A22,ENUMSET1:13; suppose A23:p in A & u in A & q = {A}; then reconsider p' = p, u' = u as Element of A; A24:f.(p,q) = d.(p',x)"\/"a by A23,Def11; A25:f.(q,u) = d.(u',x)"\/"a by A23,Def11; A26:d.(p',x) "\/" d.(u',x) <= (d.(p',x) "\/" d.(u',x))"\/"a by YELLOW_0:22; A27:(d.(p',x)"\/"d.(u',x))"\/"a = d.(p',x)"\/"(d.(u',x)"\/"a) by LATTICE3:14 .= d.(p',x)"\/"(d.(u',x)"\/"(a"\/"a)) by YELLOW_5:1 .= d.(p',x)"\/"((d.(u',x)"\/"a)"\/"a) by LATTICE3:14 .= (d.(p',x)"\/"a) "\/" (d.(u',x)"\/"a) by LATTICE3:14; d.(p',u') <= d.(p',x) "\/" d.(x,u') by A2,Def8; then d.(p',u') <= d.(p',x) "\/" d.(u',x) by A1,Def6; then d.(p',u') <= (d.(p',x)"\/"a) "\/" (d.(u',x)"\/"a) by A26,A27,ORDERS_1: 26; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A24,A25,Def11; suppose A28:p in A & u in A & q = {{A}}; then reconsider p' = p, u' = u as Element of A; A29:f.(p,q) = d.(p',x)"\/"a"\/"b by A28,Def11; A30:f.(q,u) = d.(u',x)"\/"a"\/"b by A28,Def11; A31:d.(p',x) "\/" d.(u',x) <= (d.(p',x) "\/" d.(u',x))"\/"(a"\/" b) by YELLOW_0:22; A32:(d.(p',x)"\/"d.(u',x))"\/"(a"\/"b) = d.(p',x)"\/"(d.(u',x)"\/"(a"\/" b)) by LATTICE3:14 .= d.(p',x)"\/"(d.(u',x)"\/"((a"\/"b)"\/"(a"\/"b))) by YELLOW_5:1 .= d.(p',x)"\/"((d.(u',x)"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14 .= (d.(p',x)"\/"(a"\/"b))"\/"(d.(u',x)"\/"(a"\/"b)) by LATTICE3:14 .= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"(a"\/"b)) by LATTICE3:14 .= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"a"\/"b) by LATTICE3:14; d.(p',u') <= d.(p',x) "\/" d.(x,u') by A2,Def8; then d.(p',u') <= d.(p',x) "\/" d.(u',x) by A1,Def6; then d.(p',u') <= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"a"\/" b) by A31,A32,ORDERS_1:26; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A29,A30,Def11; suppose A33:p in A & u in A & q = {{{A}}}; then reconsider p' = p, u' = u as Element of A; A34:f.(p,q) = d.(p',y)"\/"b by A33,Def11; A35:f.(q,u) = d.(u',y)"\/"b by A33,Def11; A36:d.(p',y) "\/" d.(u',y) <= (d.(p',y) "\/" d.(u',y))"\/"b by YELLOW_0:22; A37:(d.(p',y)"\/"d.(u',y))"\/"b = d.(p',y)"\/"(d.(u',y)"\/"b) by LATTICE3:14 .= d.(p',y)"\/"(d.(u',y)"\/"(b"\/"b)) by YELLOW_5:1 .= d.(p',y)"\/"((d.(u',y)"\/"b)"\/"b) by LATTICE3:14 .= (d.(p',y)"\/"b) "\/" (d.(u',y)"\/"b) by LATTICE3:14; d.(p',u') <= d.(p',y) "\/" d.(y,u') by A2,Def8; then d.(p',u') <= d.(p',y) "\/" d.(u',y) by A1,Def6; then d.(p',u') <= (d.(p',y)"\/"b) "\/" (d.(u',y)"\/"b) by A36,A37,ORDERS_1: 26; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A34,A35,Def11; end; A38: for p,q,u being Element of new_set A st p in A & q in B & u in B holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A39: p in A & q in B & u in B; then reconsider p' = p as Element of A; per cases by A39,ENUMSET1:13; suppose A40:p in A & q = {A} & u = {A}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11 .= f.(p,q) by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A40; suppose A41: p in A & q = {A} & u = {{A}}; then f.(p,u) = d.(p',x)"\/"a"\/"b by Def11 .= f.(p,q)"\/"b by A41,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A41,Def11; suppose A42:p in A & q = {A} & u = {{{A}}}; then A43:f.(p,q) = d.(p',x)"\/"a by Def11; d.(p',y) <= d.(p',x)"\/"d.(x,y) by A2,Def8; then A44: d.(p',y)"\/"b <= (d.(p',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3; A45: (d.(p',x)"\/"d.(x,y))"\/"b = (d.(p',x)"\/"b)"\/"d.(x,y) by LATTICE3:14; d.(p',x)"\/"b <= d.(p',x)"\/"b; then A46: (d.(p',x)"\/"b)"\/"d.(x,y) <= (d.(p',x)"\/"b)"\/"(a"\/" b) by A3,YELLOW_3:3; f.(p,u) <= (d.(p',x)"\/"d.(x,y))"\/"b by A42,A44,Def11; then A47: f.(p,u) <= (d.(p',x)"\/"b)"\/"(a"\/"b) by A45,A46,ORDERS_1:26; (d.(p',x)"\/"b)"\/"(a"\/"b) = d.(p',x)"\/"((b"\/"a)"\/"b) by LATTICE3:14 .= d.(p',x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14 .= d.(p',x)"\/"(a"\/"b) by YELLOW_5:1 .= d.(p',x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1 .= d.(p',x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14 .= (d.(p',x)"\/"a)"\/"(a"\/"b) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A42,A43,A47,Def11; suppose A48:p in A & q = {{A}} & u = {A}; then f.(p,q) = d.(p',x)"\/"a"\/"b by Def11 .= f.(p,u)"\/"b by A48,Def11; then f.(p,q) "\/" f.(q,u) = (f.(p,u)"\/"b)"\/"b by A48,Def11 .= f.(p,u)"\/"(b"\/"b) by LATTICE3:14 .= f.(p,u)"\/"b by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:22; suppose A49:p in A & q = {{A}} & u = {{A}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11 .= f.(p,q) by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A49; suppose A50:p in A & q = {{A}} & u = {{{A}}}; then A51:f.(p,q) = d.(p',x)"\/"a"\/"b by Def11; d.(p',y) <= d.(p',x)"\/"d.(x,y) by A2,Def8; then A52: d.(p',y)"\/"b <= (d.(p',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3; A53: (d.(p',x)"\/"d.(x,y))"\/"b = (d.(p',x)"\/"b)"\/"d.(x,y) by LATTICE3:14; d.(p',x)"\/"b <= d.(p',x)"\/"b; then A54: (d.(p',x)"\/"b)"\/"d.(x,y) <= (d.(p',x)"\/"b)"\/"(a"\/" b) by A3,YELLOW_3:3; f.(p,u) <= (d.(p',x)"\/"d.(x,y))"\/"b by A50,A52,Def11; then A55: f.(p,u) <= (d.(p',x)"\/"b)"\/"(a"\/"b) by A53,A54,ORDERS_1:26; (d.(p',x)"\/"b)"\/"(a"\/"b) = d.(p',x)"\/"((b"\/"a)"\/"b) by LATTICE3:14 .= d.(p',x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14 .= d.(p',x)"\/"(a"\/"b) by YELLOW_5:1 .= d.(p',x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1 .= d.(p',x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14 .= (d.(p',x)"\/"(a"\/"b))"\/"a by LATTICE3:14 .= (d.(p',x)"\/"a"\/"b)"\/"a by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A50,A51,A55,Def11; suppose A56:p in A & q = {{{A}}} & u = {A}; then A57:f.(p,q) = d.(p',y)"\/"b by Def11; d.(p',x) <= d.(p',y)"\/"d.(y,x) by A2,Def8; then A58: d.(p',x)"\/"a <= (d.(p',y)"\/"d.(y,x))"\/"a by WAYBEL_1:3; A59: (d.(p',y)"\/"d.(y,x))"\/"a = (d.(p',y)"\/"a)"\/"d.(y,x) by LATTICE3:14; A60:d.(y,x) <= a"\/"b by A1,A3,Def6; d.(p',y)"\/"a <= d.(p',y)"\/"a; then A61: (d.(p',y)"\/"a)"\/"d.(y,x) <= (d.(p',y)"\/"a)"\/"(a"\/" b) by A60,YELLOW_3:3; f.(p,u) <= (d.(p',y)"\/"d.(y,x))"\/"a by A56,A58,Def11; then A62: f.(p,u) <= (d.(p',y)"\/"a)"\/"(a"\/"b) by A59,A61,ORDERS_1:26; (d.(p',y)"\/"a)"\/"(a"\/"b) = (d.(p',y)"\/"a"\/"a)"\/"b by LATTICE3:14 .=(d.(p',y)"\/"(a"\/"a))"\/" b by LATTICE3:14 .= (d.(p',y)"\/"a)"\/"b by YELLOW_5:1 .= d.(p',y)"\/"(a"\/"b) by LATTICE3:14 .= d.(p',y)"\/"(a"\/"(b"\/"b)) by YELLOW_5:1 .= d.(p',y)"\/"((a"\/"b)"\/"b) by LATTICE3:14 .= (d.(p',y)"\/"b)"\/"(a"\/"b) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A56,A57,A62,Def11; suppose A63:p in A & q = {{{A}}} & u = {{A}}; then A64:f.(p,u) = d.(p',x)"\/"a"\/"b by Def11; A65:f.(p,q) = d.(p',y)"\/"b by A63,Def11; d.(p',x) <= d.(p',y)"\/"d.(y,x) by A2,Def8; then A66: d.(p',x)"\/"(a"\/"b) <= (d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) by WAYBEL_1:3; A67: (d.(p',y)"\/"a)"\/"(a"\/"b) = (d.(p',y)"\/"a)"\/"((a"\/"b)"\/"(a"\/" b)) by YELLOW_5:1 .= d.(p',y)"\/"(a"\/"((a"\/"b)"\/"(a"\/"b))) by LATTICE3:14 .= d.(p',y)"\/"((a"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14 .= d.(p',y)"\/"(((a"\/"a)"\/"b)"\/"(a"\/"b)) by LATTICE3:14 .= d.(p',y)"\/"((a"\/"b)"\/"(a"\/"b)) by YELLOW_5:1 .= (d.(p',y)"\/"(a"\/"b))"\/"(a"\/"b) by LATTICE3:14; A68:d.(y,x) <= a"\/"b by A1,A3,Def6; A69:(d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) = (d.(p',y)"\/"(a"\/"b))"\/" d.(y,x) by LATTICE3:14; d.(p',y)"\/"(a"\/"b) <= d.(p',y)"\/"(a"\/"b); then A70:(d.(p',y)"\/"d.(y,x))"\/"(a"\/"b)<=(d.(p',y)"\/"(a"\/"b))"\/"(a"\/" b) by A68,A69,YELLOW_3:3; f.(p,u) <= (d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) by A64,A66,LATTICE3:14; then A71: f.(p,u) <= (d.(p',y)"\/"a)"\/"(a"\/"b) by A67,A70,ORDERS_1:26; (d.(p',y)"\/"a)"\/"(a"\/"b) = (d.(p',y)"\/"a"\/"a)"\/"b by LATTICE3:14 .=(d.(p',y)"\/"(a"\/"a))"\/" b by LATTICE3:14 .= (d.(p',y)"\/"a)"\/"b by YELLOW_5:1 .= (d.(p',y)"\/"b)"\/" a by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A63,A65,A71,Def11; suppose A72:p in A & q = {{{A}}} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11 .= f.(p,q) by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A72; end; A73: for p,q,u being Element of new_set A st p in B & q in A & u in A holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A74:p in B & q in A & u in A; then reconsider q' = q, u' = u as Element of A; per cases by A74,ENUMSET1:13; suppose A75:p = {A} & q in A & u in A; then A76:f.(p,q) = d.(q',x)"\/"a by Def11; A77:f.(q,u) = d.(q',u') by Def11; d.(u',x) <= d.(u',q') "\/" d.(q',x) by A2,Def8; then d.(u',x) <= d.(q',u') "\/" d.(q',x) by A1,Def6; then d.(u',x)"\/"a <= (d.(q',x)"\/"d.(q',u'))"\/"a by WAYBEL_1:3; then d.(u',x)"\/"a <= (d.(q',x)"\/"a)"\/"d.(q',u') by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A75,A76,A77,Def11; suppose A78:p = {{A}} & q in A & u in A; then A79:f.(p,q) = d.(q',x)"\/"a"\/"b by Def11; A80:f.(q,u) = d.(q',u') by Def11; d.(u',x) <= d.(u',q') "\/" d.(q',x) by A2,Def8; then d.(u',x) <= d.(q',u') "\/" d.(q',x) by A1,Def6; then d.(u',x)"\/"(a"\/"b) <= (d.(q',x)"\/"d.(q',u'))"\/"(a"\/" b) by WAYBEL_1:3; then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"d.(q',u'))"\/"(a"\/" b) by LATTICE3:14; then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"(a"\/"b))"\/" d.(q',u') by LATTICE3:14; then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"a"\/"b)"\/"d.(q',u') by LATTICE3:14 ; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A78,A79,A80,Def11; suppose A81:p = {{{A}}} & q in A & u in A; then A82:f.(p,q) = d.(q',y)"\/"b by Def11; A83:f.(q,u) = d.(q',u') by Def11; d.(u',y) <= d.(u',q') "\/" d.(q',y) by A2,Def8; then d.(u',y) <= d.(q',u') "\/" d.(q',y) by A1,Def6; then d.(u',y)"\/"b <= (d.(q',y)"\/"d.(q',u'))"\/"b by WAYBEL_1:3; then d.(u',y)"\/"b <= (d.(q',y)"\/"b)"\/"d.(q',u') by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A81,A82,A83,Def11; end; A84: for p,q,u being Element of new_set A st p in B & q in A & u in B holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A85: p in B & q in A & u in B; then reconsider q' = q as Element of A; per cases by A85,ENUMSET1:13; suppose q in A & p = {A} & u = {A}; then f.(p,u) = Bottom L by Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; suppose A86:q in A & p = {A} & u = {{A}}; then A87:f.(p,u) = b by Def11; f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q',x)"\/"a"\/"b) by A86,Def11 .= f.(p,q)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14 .= (f.(p,q)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14 .= ((f.(p,q)"\/"d.(q',x))"\/"a)"\/"b by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A87,YELLOW_0:22; suppose A88:q in A & p = {A} & u = {{{A}}}; then A89:f.(p,u) = a"\/"b by Def11; f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a)"\/"f.(q,u) by A88,Def11 .= (d.(q',x)"\/"a)"\/"(d.(q',y)"\/"b) by A88,Def11 .= d.(q',x)"\/"(a"\/"(d.(q',y)"\/"b)) by LATTICE3:14 .= d.(q',x)"\/"(d.(q',y)"\/"(a"\/"b)) by LATTICE3:14 .= (d.(q',x)"\/"d.(q',y))"\/"(a"\/"b) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A89,YELLOW_0:22; suppose A90:q in A & p = {{A}} & u = {A}; then A91:f.(p,u) = b by Def11; f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a"\/"b)"\/"f.(q,u) by A90,Def11 .= f.(q,u)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14 .= (f.(q,u)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14 .= ((f.(q,u)"\/"d.(q',x))"\/"a)"\/"b by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A91,YELLOW_0:22; suppose q in A & p = {{A}} & u = {{A}}; then f.(p,u) = Bottom L by Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; suppose A92:q in A & p = {{A}} & u = {{{A}}}; then A93:f.(p,u) = a by Def11; f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a"\/"b)"\/"f.(q,u) by A92,Def11 .= (a"\/"(d.(q',x)"\/"b))"\/"f.(q,u) by LATTICE3:14 .= a"\/"((d.(q',x)"\/"b)"\/"f.(q,u)) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A93,YELLOW_0:22; suppose A94:q in A & p = {{{A}}} & u = {A}; then A95:f.(p,u) = a"\/"b by Def11; f.(p,q) "\/" f.(q,u) = (d.(q',y)"\/"b)"\/"f.(q,u) by A94,Def11 .= (d.(q',y)"\/"b)"\/"(d.(q',x)"\/"a) by A94,Def11 .= d.(q',y)"\/"(b"\/"(d.(q',x)"\/"a)) by LATTICE3:14 .= d.(q',y)"\/"(d.(q',x)"\/"(b"\/"a)) by LATTICE3:14 .= (d.(q',y)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A95,YELLOW_0:22; suppose A96:q in A & p = {{{A}}} & u = {{A}}; then A97:f.(p,u) = a by Def11; f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q',x)"\/"a"\/"b) by A96,Def11 .= f.(p,q)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14 .= (f.(p,q)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14 .= ((f.(p,q)"\/"d.(q',x))"\/"b)"\/"a by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A97,YELLOW_0:22; suppose q in A & p = {{{A}}} & u = {{{A}}}; then f.(p,u) = Bottom L by Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; end; A98: for p,q,u being Element of new_set A st p in B & q in B & u in A holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A99: p in B & q in B & u in A; then reconsider u' = u as Element of A; per cases by A99,ENUMSET1:13; suppose A100:u in A & q = {A} & p = {A}; then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def11 .= f.(p,u) by A100,WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u); suppose A101:u in A & q = {A} & p = {{A}}; then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def11 .= d.(u',x)"\/"a"\/" b by A101,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A101,Def11; suppose A102:u in A & q = {A} & p = {{{A}}}; then A103:f.(p,u) = d.(u',y)"\/"b by Def11; d.(u',y) <= d.(u',x)"\/"d.(x,y) by A2,Def8; then A104:d.(u',y)"\/"b <= (d.(u',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3; A105:(d.(u',x)"\/"d.(x,y))"\/"b = (d.(u',x)"\/"b)"\/"d.(x,y) by LATTICE3:14; d.(u',x)"\/"b <= d.(u',x)"\/"b; then (d.(u',x)"\/"b)"\/"d.(x,y) <= (d.(u',x)"\/"b)"\/"(a"\/" b) by A3,YELLOW_3:3; then A106:f.(p,u) <= (d.(u',x)"\/"b)"\/"(a"\/"b) by A103,A104,A105,ORDERS_1:26; b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14 .= b"\/"a by YELLOW_5:1 .= b"\/"(a"\/"a) by YELLOW_5:1 .= a"\/"(a"\/"b) by LATTICE3:14; then (d.(u',x)"\/"b)"\/"(a"\/"b) = d.(u',x)"\/"(a"\/"(a"\/" b)) by LATTICE3:14 .= (a"\/"b)"\/"(d.(u',x)"\/"a) by LATTICE3:14 .= f.(p,q)"\/"(d.(u',x)"\/" a) by A102,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A102,A106,Def11; suppose A107:u in A & q = {{A}} & p = {A}; then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def11 .= b"\/"(d.(u',x)"\/"a"\/" b) by A107,Def11 .= b"\/"(b"\/"f.(p,u)) by A107,Def11 .= (b"\/"b)"\/"f.(p,u) by LATTICE3:14 .= b"\/"f.(p,u) by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:22; suppose A108:u in A & q = {{A}} & p = {{A}}; then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def11 .= f.(p,u) by A108,WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u); suppose A109:u in A & q = {{A}} & p = {{{A}}}; then A110:f.(p,u) = d.(u',y)"\/"b by Def11; d.(u',y) <= d.(u',x)"\/"d.(x,y) by A2,Def8; then A111:d.(u',y)"\/"b <= (d.(u',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3; A112:(d.(u',x)"\/"d.(x,y))"\/"b = (d.(u',x)"\/"b)"\/"d.(x,y) by LATTICE3:14; A113:b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14 .= b"\/"a by YELLOW_5:1 .= b"\/"(a"\/"a) by YELLOW_5:1 .= (a"\/"b)"\/"a by LATTICE3:14; d.(u',x)"\/"b <= d.(u',x)"\/"b; then (d.(u',x)"\/"b)"\/"d.(x,y) <= (d.(u',x)"\/"b)"\/"(a"\/" b) by A3,YELLOW_3:3; then A114:f.(p,u) <= (d.(u',x)"\/"b)"\/"(a"\/"b) by A110,A111,A112,ORDERS_1:26; (d.(u',x)"\/"b)"\/"(a"\/"b) = d.(u',x)"\/"((a"\/"b)"\/"a) by A113,LATTICE3 :14 .= (d.(u',x)"\/"(a"\/"b))"\/"a by LATTICE3:14 .= (d.(u',x)"\/"a"\/"b)"\/"a by LATTICE3:14 .= f.(p,q)"\/"(d.(u',x)"\/"a"\/"b) by A109,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A109,A114,Def11; suppose A115:u in A & q = {{{A}}} & p = {A}; then A116:f.(p,u) = d.(u',x)"\/"a by Def11; d.(u',x) <= d.(u',y)"\/"d.(y,x) by A2,Def8; then A117:d.(u',x)"\/"a <= (d.(u',y)"\/"d.(y,x))"\/"a by WAYBEL_1:3; A118:(d.(u',y)"\/"d.(y,x))"\/"a = d.(y,x)"\/"(d.(u',y)"\/"a) by LATTICE3:14 .= (a"\/"d.(u',y))"\/"d.(x,y) by A1,Def6; A119:a"\/"(a"\/"b) = (a"\/"a)"\/"b by LATTICE3:14 .= a"\/"b by YELLOW_5:1 .= a"\/"(b"\/"b) by YELLOW_5:1 .= b"\/"(a"\/"b) by LATTICE3:14; a"\/"d.(u',y) <= a"\/"d.(u',y); then (a"\/"d.(u',y))"\/"d.(x,y) <= (a"\/"d.(u',y))"\/"(a"\/" b) by A3,YELLOW_3:3; then A120:f.(p,u) <= (a"\/"d.(u',y))"\/"(a"\/"b) by A116,A117,A118,ORDERS_1:26; (a"\/"d.(u',y))"\/"(a"\/"b) = d.(u',y)"\/"(a"\/"(a"\/"b)) by LATTICE3:14 .= (d.(u',y)"\/"b)"\/"(a"\/"b) by A119,LATTICE3:14 .= f.(p,q)"\/"(d.(u',y)"\/"b) by A115,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A115,A120,Def11; suppose A121:u in A & q = {{{A}}} & p = {{A}}; then A122:f.(p,u) = d.(u',x)"\/"a"\/"b by Def11 .= d.(u',x)"\/"(a"\/" b) by LATTICE3:14; d.(u',x) <= d.(u',y)"\/"d.(y,x) by A2,Def8; then A123:d.(u',x)"\/"(a"\/"b) <= (d.(u',y)"\/"d.(y,x))"\/"(a"\/"b) by WAYBEL_1 :3; A124:(d.(u',y)"\/"d.(y,x))"\/"(a"\/"b) = ((a"\/"b)"\/"d.(u',y))"\/" d.(y,x) by LATTICE3:14 .= ((a"\/"b)"\/"d.(u',y))"\/"d.(x,y) by A1,Def6; (a"\/"b)"\/"d.(u',y) <= (a"\/"b)"\/"d.(u',y); then A125:((a"\/"b)"\/"d.(u',y))"\/"d.(x,y) <= ((a"\/"b)"\/"d.(u',y))"\/"(a"\/"b) by A3,YELLOW_3:3; f.(p,q)"\/"f.(q,u) = a"\/"f.(q,u) by A121,Def11 .= a"\/"(b"\/" d.(u',y)) by A121,Def11 .= (a"\/"b)"\/"d.(u',y) by LATTICE3:14 .= ((a"\/"b)"\/"(a"\/"b))"\/"d.(u',y) by YELLOW_5:1 .= (a"\/"b)"\/"(d.(u',y)"\/"(a"\/"b)) by LATTICE3:14; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A122,A123,A124,A125,ORDERS_1:26; suppose A126:u in A & q = {{{A}}} & p = {{{A}}}; then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def11 .= f.(p,u) by A126,WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u); end; A127: for p,q,u being Element of new_set A st p in B & q in B & u in B holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; assume A128:p in B & q in B & u in B; per cases by A128,ENUMSET1:13; suppose A129: p = {A} & q = {A} & u = {A}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A129,Def11; suppose A130: p = {A} & q = {A} & u = {{A}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def11 .= Bottom L"\/"b by A130,Def11 .= b by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A130,Def11; suppose A131: p = {A} & q = {A} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def11 .= Bottom L"\/"(a"\/"b) by A131,Def11 .= a"\/"b by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A131,Def11; suppose A132: p = {A} & q = {{A}} & u = {A}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A132,Def11; suppose A133: p = {A} & q = {{A}} & u = {{A}}; then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def11 .= Bottom L"\/"b by A133, Def11 .= b by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A133,Def11; suppose A134: p = {A} & q = {{A}} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def11 .= a"\/"b by A134,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A134,Def11; suppose A135: p = {A} & q = {{{A}}} & u = {A}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A135,Def11; suppose A136: p = {A} & q = {{{A}}} & u = {{A}}; then A137:f.(p,u) = b by Def11; f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A136,Def11 .= (b"\/"a)"\/" a by A136,Def11 .= b"\/"(a"\/"a) by LATTICE3:14 .= b"\/"a by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A137,YELLOW_0:22; suppose A138: p = {A} & q = {{{A}}} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def11 .= Bottom L"\/"(a "\/" b) by A138,Def11 .= a"\/"b by WAYBEL_1:4 .= f.(p,q) by A138,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A138; suppose A139: p = {{A}} & q = {A} & u = {A}; then f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by Def11 .= Bottom L"\/"b by A139, Def11 .= b by WAYBEL_1:4 .= f.(p,q) by A139,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A139; suppose A140: p = {{A}} & q = {A} & u = {{A}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A140,Def11; suppose A141: p = {{A}} & q = {A} & u = {{{A}}}; then A142:f.(p,u) = a by Def11; f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by A141,Def11 .= b"\/"(b"\/" a) by A141,Def11 .= (b"\/"b)"\/"a by LATTICE3:14 .= b"\/"a by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A142,YELLOW_0:22; suppose A143: p = {{A}} & q = {{A}} & u = {A}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11 .= Bottom L"\/"b by A143,Def11 .= b by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A143,Def11; suppose A144: p = {{A}} & q = {{A}} & u = {{A}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A144,Def11; suppose A145: p = {{A}} & q = {{A}} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11 .= Bottom L"\/"a by A145,Def11 .= a by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A145,Def11; suppose A146: p = {{A}} & q = {{{A}}} & u = {A}; then A147:f.(p,u) = b by Def11; f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by A146,Def11 .= a"\/"(a"\/" b) by A146,Def11 .= (a"\/"a)"\/"b by LATTICE3:14 .= a"\/"b by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A147,YELLOW_0:22; suppose A148: p = {{A}} & q = {{{A}}} & u = {{A}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A148,Def11; suppose A149: p = {{A}} & q = {{{A}}} & u = {{{A}}}; then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= Bottom L"\/"a by A149, Def11 .= a by WAYBEL_1:4 .= f.(p,q) by A149,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A149; suppose A150: p = {{{A}}} & q = {A} & u = {A}; then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def11 .= Bottom L"\/"(a "\/" b) by A150,Def11 .= a"\/"b by WAYBEL_1:4 .= f.(p,q) by A150,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A150; suppose A151: p = {{{A}}} & q = {A} & u = {{A}}; then A152:f.(p,u) = a by Def11; f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A151,Def11 .= (a"\/"b)"\/" b by A151,Def11 .= a"\/"(b"\/"b) by LATTICE3:14 .= a"\/"b by YELLOW_5:1; hence f.(p,u) <= f.(p,q) "\/" f.(q,u)by A152,YELLOW_0:22; suppose A153: p = {{{A}}} & q = {A} & u = {{{A}}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A153,Def11; suppose A154: p = {{{A}}} & q = {{A}} & u = {A}; then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= a"\/"b by A154,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A154,Def11; suppose A155: p = {{{A}}} & q = {{A}} & u = {{A}}; then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= Bottom L"\/"a by A155, Def11 .= a by WAYBEL_1:4 .= f.(p,q) by A155,Def11; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A155; suppose A156: p = {{{A}}} & q = {{A}} & u = {{{A}}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A156,Def11; suppose A157: p = {{{A}}} & q = {{{A}}} & u = {A}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11 .= Bottom L"\/"(a"\/"b) by A157,Def11 .= a"\/"b by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A157,Def11; suppose A158: p = {{{A}}} & q = {{{A}}} & u = {{A}}; then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11 .= Bottom L"\/"a by A158,Def11 .= a by WAYBEL_1:4; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A158,Def11; suppose A159: p = {{{A}}} & q = {{{A}}} & u = {{{A}}}; Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A159,Def11; end; for p,q,u being Element of new_set A holds f.(p,u) <= f.(p,q) "\/" f.(q,u) proof let p,q,u be Element of new_set A; p in new_set A & q in new_set A & u in new_set A; then A160: p in A \/ B & q in A \/ B & u in A \/ B by Def10; per cases by A160,XBOOLE_0:def 2; suppose p in A & q in A & u in A; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A4; suppose p in A & q in A & u in B; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A7; suppose p in A & q in B & u in A; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A21; suppose p in A & q in B & u in B; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A38; suppose p in B & q in A & u in A; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A73; suppose p in B & q in A & u in B; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A84; suppose p in B & q in B & u in A; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A98; suppose p in B & q in B & u in B; hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A127; end; hence f is u.t.i. by Def8; end; theorem Th21: for A be set holds A c= new_set A proof let A be set; A c= A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_1:7; hence thesis by Def10; end; theorem Th22: for d be BiFunction of A,L for q be Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun(d,q) proof let d be BiFunction of A,L; let q be Element of [:A,A,the carrier of L,the carrier of L:]; set g = new_bi_fun(d,q); A1: dom d = [:A,A:] & dom g = [:new_set A,new_set A:] by FUNCT_2:def 1; A c= new_set A by Th21; then A2: dom d c= dom g by A1,ZFMISC_1:119; for z being set st z in dom d holds d.z = g.z proof let z be set; assume A3: z in dom d; then consider x,y such that A4: [x,y] = z by ZFMISC_1:102; reconsider x' = x, y' = y as Element of A by A3,A4,ZFMISC_1:106; d.[x,y] = d.(x',y') by BINOP_1:def 1 .= g.(x',y') by Def11 .= g.[x,y] by BINOP_1:def 1; hence d.z = g.z by A4; end; hence d c= new_bi_fun(d,q) by A2,GRFUNC_1:8; end; definition let A,L; let d be BiFunction of A,L; func DistEsti(d) -> Cardinal means :Def12: it,{ [x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} are_equipotent; existence proof set D = { [x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; take Card D; thus Card D,D are_equipotent by CARD_1:def 5; end; uniqueness proof set D = { [x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; let c1,c2 be Cardinal such that A1: c1,D are_equipotent and A2: c2,D are_equipotent; c1,c2 are_equipotent by A1,A2,WELLORD2:22; hence c1 = c2 by CARD_1:8; end; end; theorem Th23: for d be distance_function of A,L holds DistEsti(d) <> {} proof let d be distance_function of A,L; set X = { [x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; consider x' being Element of A; consider z being set such that A1: z = [x',x',Bottom L,Bottom L]; d.(x',x') = Bottom L by Def7 .= Bottom L "\/" Bottom L by YELLOW_5:1; then A2: z in X by A1; DistEsti(d),X are_equipotent by Def12; hence DistEsti(d) <> {} by A2,CARD_1:46; end; reserve T,L1,LL for T-Sequence, O,O1,O2,O3,C for Ordinal; definition let A; let O; func ConsecutiveSet(A,O) means :Def13: ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = A & (for C being Ordinal st succ C in succ O holds L0.succ C = new_set L0.C) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = union rng (L0|C); correctness proof deffunc C(Ordinal,set) = new_set $2; deffunc D(Ordinal,T-Sequence) = union rng $2; thus (ex x,L1 st x = last L1 & dom L1 = succ O & L1.{} = A & (for C being Ordinal st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) & for x1,x2 being set st (ex L1 st x1 = last L1 & dom L1 = succ O & L1.{} = A & (for C st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) & (ex L1 st x2 = last L1 & dom L1 = succ O & L1.{} = A & (for C st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) holds x1 = x2 from TS_Def; end; end; theorem Th24: ConsecutiveSet(A,{}) = A proof deffunc U(Ordinal,set) = new_set $2; deffunc V(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveSet(A,$1); A1: for O being Ordinal, x being set holds x = F(O) iff ex L0 being T-Sequence st x = last L0 & dom L0 = succ O & L0.{} = A & (for C being Ordinal st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = V(C,L0|C) by Def13; thus F({}) = A from TS_Result0(A1); end; theorem Th25: ConsecutiveSet(A,succ O) = new_set ConsecutiveSet(A,O) proof deffunc U(Ordinal,set) = new_set $2; deffunc V(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveSet(A,$1); A1: for O being Ordinal, It being set holds It = F(O) iff ex L0 being T-Sequence st It = last L0 & dom L0 = succ O & L0.{} = A & (for C being Ordinal st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = V(C,L0|C) by Def13; for O holds F(succ O) = U(O,F(O)) from TS_ResultS(A1); hence thesis; end; theorem Th26: O <> {} & O is_limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveSet(A,O1)) implies ConsecutiveSet(A,O) = union rng T proof deffunc U(Ordinal,set) = new_set $2; deffunc V(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveSet(A,$1); assume that A1: O <> {} & O is_limit_ordinal and A2: dom T = O and A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1); A4: for O being Ordinal, x being set holds x = F(O) iff ex L0 being T-Sequence st x = last L0 & dom L0 = succ O & L0.{} = A & (for C being Ordinal st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = V(C,L0|C) by Def13; thus F(O) = V(O,T) from TS_ResultL(A4,A1,A2,A3); end; definition let A; let O; cluster ConsecutiveSet(A,O) -> non empty; coherence proof defpred X[Ordinal] means ConsecutiveSet(A,$1) is non empty; A1: X[{}] by Th24; A2: for O st X[O] holds X[succ O] proof let O1; assume ConsecutiveSet(A,O1) is non empty; ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25; hence ConsecutiveSet(A,succ O1) is non empty; end; A3: for O st O <> {} & O is_limit_ordinal & for B being Ordinal st B in O holds X[B] holds X[O] proof let O1; assume A4: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds ConsecutiveSet(A,O2) is non empty; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ls being T-Sequence such that A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(O2) from TS_Lambda; A6: ConsecutiveSet(A,O1) = union rng Ls by A4,A5,Th26; A7: {} in O1 by A4,ORDINAL3:10; then Ls.{} = ConsecutiveSet(A,{}) by A5 .= A by Th24; then A in rng Ls by A5,A7,FUNCT_1:def 5; then A8: A c= ConsecutiveSet(A,O1) by A6,ZFMISC_1:92; consider x being set such that A9:x in A by XBOOLE_0:def 1; thus ConsecutiveSet(A,O1) is non empty by A8,A9; end; for O holds X[O] from Ordinal_Ind(A1,A2,A3); hence thesis; end; end; theorem Th27: A c= ConsecutiveSet(A,O) proof defpred X[Ordinal] means A c= ConsecutiveSet(A,$1); A1: X[{}] by Th24; A2: for O1 st X[O1] holds X[succ O1] proof let O1; assume A3: A c= ConsecutiveSet(A,O1); ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25; then ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O1) by Th21; hence A c= ConsecutiveSet(A,succ O1) by A3,XBOOLE_1:1; end; A4: for O2 st O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2] proof let O2; assume A5: O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds A c= ConsecutiveSet(A,O1); deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ls being T-Sequence such that A6: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1) from TS_Lambda; A7: ConsecutiveSet(A,O2) = union rng Ls by A5,A6,Th26; A8: {} in O2 by A5,ORDINAL3:10; then Ls.{} = ConsecutiveSet(A,{}) by A6 .= A by Th24; then A in rng Ls by A6,A8,FUNCT_1:def 5; hence A c= ConsecutiveSet(A,O2) by A7,ZFMISC_1:92; end; for O holds X[O] from Ordinal_Ind(A1,A2,A4); hence thesis; end; definition let A,L; let d be BiFunction of A,L; mode QuadrSeq of d -> T-Sequence of [:A,A,the carrier of L,the carrier of L:] means :Def14: dom it is Cardinal & it is one-to-one & rng it ={[x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; existence proof set X = {[x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; Card X,X are_equipotent by CARD_1:def 5; then consider f being Function such that A1: f is one-to-one and A2: dom f = Card X and A3: rng f = X by WELLORD2:def 4; reconsider f as T-Sequence by A2,ORDINAL1:def 7; rng f c= [:A,A,the carrier of L,the carrier of L:] proof let z be set; assume z in rng f; then consider x,y being Element of A, a,b being Element of L such that A4: z = [x,y,a,b] & d.(x,y) <= a"\/"b by A3; thus z in [:A,A,the carrier of L,the carrier of L:] by A4; end; then reconsider f as T-Sequence of [:A,A,the carrier of L,the carrier of L:] by ORDINAL1:def 8; take f; thus dom f is Cardinal by A2; thus f is one-to-one by A1; thus rng f = X by A3; end; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; assume A1: O in dom q; func Quadr(q,O) -> Element of [:ConsecutiveSet(A,O),ConsecutiveSet(A,O), the carrier of L,the carrier of L:] equals :Def15: q.O; correctness proof q.O in rng q by A1,FUNCT_1:def 5; then q.O in {[x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} by Def14; then consider x,y be Element of A, a,b be Element of L such that A2: q.O = [x,y,a,b] & d.(x,y) <= a"\/"b; A3: x in A & y in A; A c= ConsecutiveSet(A,O) by Th27; then reconsider x,y as Element of ConsecutiveSet(A,O) by A3; reconsider a,b as Element of L; reconsider z = [x,y,a,b] as Element of [:ConsecutiveSet(A,O),ConsecutiveSet(A,O), the carrier of L,the carrier of L:]; z = q.O by A2; hence thesis; end; end; theorem Th28: for d being BiFunction of A,L, q being QuadrSeq of d holds O in DistEsti(d) iff O in dom q proof let d be BiFunction of A,L; let q be QuadrSeq of d; DistEsti(d),{[x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} are_equipotent by Def12; then A1: DistEsti(d),rng q are_equipotent by Def14; q is one-to-one by Def14; then dom q,rng q are_equipotent by WELLORD2:def 4; then A2: DistEsti(d),dom q are_equipotent by A1,WELLORD2:22; reconsider M = DistEsti(d) as Cardinal; reconsider N = dom q as Cardinal by Def14; A3: M = N by A2,CARD_1:8; hence O in DistEsti(d) implies O in dom q; assume O in dom q; hence O in DistEsti(d) by A3; end; definition let A,L; let z be set; assume A1: z is BiFunction of A,L; func BiFun(z,A,L) -> BiFunction of A,L equals :Def16: z; coherence by A1; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; func ConsecutiveDelta(q,O) means :Def17: ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = d & (for C being Ordinal st succ C in succ O holds L0.succ C = new_bi_fun(BiFun(L0.C,ConsecutiveSet(A,C),L),Quadr(q,C))) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = union rng(L0|C); correctness proof deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1)); deffunc D(Ordinal,T-Sequence) = union rng $2; thus (ex x,L1 st x = last L1 & dom L1 = succ O & L1.{} = d & (for C being Ordinal st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) & for x1,x2 being set st (ex L1 st x1 = last L1 & dom L1 = succ O & L1.{} = d & (for C st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) & (ex L1 st x2 = last L1 & dom L1 = succ O & L1.{} = d & (for C st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C) ) holds x1 = x2 from TS_Def; end; end; theorem Th29: for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,{}) = d proof let d be BiFunction of A,L, q be QuadrSeq of d; deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1)); deffunc D(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveDelta(q,$1); A1: for O being Ordinal, It being set holds It = F(O) iff ex L0 being T-Sequence st It = last L0 & dom L0 = succ O & L0.{} = d & (for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = D(C,L0|C) by Def17; thus F({}) = d from TS_Result0(A1); end; theorem Th30: for d be BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,succ O) = new_bi_fun(BiFun(ConsecutiveDelta(q,O), ConsecutiveSet(A,O),L),Quadr(q,O)) proof let d be BiFunction of A,L; let q be QuadrSeq of d; deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1)); deffunc D(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveDelta(q,$1); A1: for O being Ordinal, It being set holds It = F(O) iff ex L0 being T-Sequence st It = last L0 & dom L0 = succ O & L0.{} = d & (for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = D(C,L0|C) by Def17; for O holds F(succ O) = C(O,F(O)) from TS_ResultS(A1); hence thesis; end; theorem Th31: for d be BiFunction of A,L for q being QuadrSeq of d holds O <> {} & O is_limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveDelta(q,O1)) implies ConsecutiveDelta(q,O) = union rng T proof let d be BiFunction of A,L; let q be QuadrSeq of d; deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1)); deffunc D(Ordinal,T-Sequence) = union rng $2; deffunc F(Ordinal) = ConsecutiveDelta(q,$1); assume that A1: O <> {} & O is_limit_ordinal and A2: dom T = O and A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1); A4: for O being Ordinal, It being set holds It = F(O) iff ex L0 being T-Sequence st It = last L0 & dom L0 = succ O & L0.{} = d & (for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = D(C,L0|C) by Def17; thus F(O) = D(O,T) from TS_ResultL(A4,A1,A2,A3); end; theorem Th32: O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2) proof defpred X[Ordinal] means O1 c= $1 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,$1); A1: X[{}] by XBOOLE_1:3; A2: for O2 st X[O2] holds X[succ O2] proof let O2; assume A3: O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2); assume A4: O1 c= succ O2; per cases; suppose O1 = succ O2; hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O2); suppose O1 <> succ O2; then O1 c< succ O2 by A4,XBOOLE_0:def 8; then A5: O1 in succ O2 by ORDINAL1:21; ConsecutiveSet(A,O2) c= new_set ConsecutiveSet(A,O2) by Th21; then ConsecutiveSet(A,O1) c= new_set ConsecutiveSet(A,O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1; hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O2) by Th25; end; A6: for O2 st O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2] proof let O2; assume A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds O1 c= O3 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O3); assume A8: O1 c= O2; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider L being T-Sequence such that A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3) from TS_Lambda; A10: ConsecutiveSet(A,O2) = union rng L by A7,A9,Th26; per cases; suppose O1 = O2; hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2); suppose O1 <> O2; then O1 c< O2 by A8,XBOOLE_0:def 8; then A11: O1 in O2 by ORDINAL1:21; then A12: L.O1 = ConsecutiveSet(A,O1) by A9; L.O1 in rng L by A9,A11,FUNCT_1:def 5; hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2) by A10,A12,ZFMISC_1:92; end; for O2 holds X[O2] from Ordinal_Ind(A1,A2,A6); hence thesis; end; theorem Th33: for d be BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is BiFunction of ConsecutiveSet(A,O),L proof let d be BiFunction of A,L; let q be QuadrSeq of d; defpred Y[Ordinal] means ConsecutiveDelta(q,$1) is BiFunction of ConsecutiveSet(A,$1),L; A1: Y[{}] proof ConsecutiveDelta(q,{}) = d & ConsecutiveSet(A,{}) = A by Th24,Th29; hence ConsecutiveDelta(q,{}) is BiFunction of ConsecutiveSet(A,{}),L; end; A2: for O1 st Y[O1] holds Y[succ O1] proof let O1; assume ConsecutiveDelta(q,O1) is BiFunction of ConsecutiveSet(A,O1),L; then reconsider CD = ConsecutiveDelta(q,O1) as BiFunction of ConsecutiveSet(A,O1),L; X: ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25; ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1), ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .= new_bi_fun(CD,Quadr(q,O1)) by Def16; hence ConsecutiveDelta(q,succ O1) is BiFunction of ConsecutiveSet(A,succ O1),L by X; end; A3: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds Y[O2] holds Y[O1] proof let O1; assume A4: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds ConsecutiveDelta(q,O2) is BiFunction of ConsecutiveSet(A,O2),L; deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Ls being T-Sequence such that A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(O2) from TS_Lambda; A6: ConsecutiveDelta(q,O1) = union rng Ls by A4,A5,Th31; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ts being T-Sequence such that A7: dom Ts = O1 & for O2 being Ordinal st O2 in O1 holds Ts.O2 = U(O2) from TS_Lambda; set CS = ConsecutiveSet(A,O1), Y = the carrier of L, X = [:ConsecutiveSet(A,O1),ConsecutiveSet(A,O1):], f = union rng Ls; A8: for O,O2 st O c= O2 & O2 in dom Ls holds Ls.O c= Ls.O2 proof let O; defpred X[Ordinal] means O c= $1 & $1 in dom Ls implies Ls.O c= Ls.$1; A9: X[{}] by XBOOLE_1:3; A10: for O2 st X[O2] holds X[succ O2] proof let O2; assume A11: O c= O2 & O2 in dom Ls implies Ls.O c= Ls.O2; assume that A12: O c= succ O2 and A13: succ O2 in dom Ls; per cases; suppose O = succ O2; hence Ls.O c= Ls.succ O2; suppose O <> succ O2; then O c< succ O2 by A12,XBOOLE_0:def 8; then A14: O in succ O2 by ORDINAL1:21; A15: O2 in succ O2 by ORDINAL1:10; then A16: O2 in dom Ls by A13,ORDINAL1:19; then reconsider cd2 = ConsecutiveDelta(q,O2) as BiFunction of ConsecutiveSet(A,O2),L by A4,A5; Ls.succ O2 = ConsecutiveDelta(q,succ O2) by A5,A13 .= new_bi_fun(BiFun(ConsecutiveDelta(q,O2), ConsecutiveSet(A,O2),L),Quadr(q,O2)) by Th30 .= new_bi_fun(cd2,Quadr(q,O2)) by Def16; then ConsecutiveDelta(q,O2) c= Ls.succ O2 by Th22; then Ls.O2 c= Ls.succ O2 by A5,A16; hence Ls.O c= Ls.succ O2 by A11,A13,A14,A15,ORDINAL1:19,34,XBOOLE_1:1 ; end; A17: for O2 st O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2] proof let O2; assume that A18: O2 <> {} & O2 is_limit_ordinal and for O3 st O3 in O2 holds O c= O3 & O3 in dom Ls implies Ls.O c= Ls.O3; assume that A19: O c= O2 and A20: O2 in dom Ls; deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Lt being T-Sequence such that A21: dom Lt = O2 & for O3 being Ordinal st O3 in O2 holds Lt.O3 = U(O3) from TS_Lambda; A22:Ls.O2 = ConsecutiveDelta(q,O2) by A5,A20 .= union rng Lt by A18,A21,Th31; per cases; suppose O = O2; hence Ls.O c= Ls.O2; suppose O <> O2; then O c< O2 by A19,XBOOLE_0:def 8; then A23: O in O2 by ORDINAL1:21; then O in O1 by A5,A20,ORDINAL1:19; then Ls.O = ConsecutiveDelta(q,O) by A5 .= Lt.O by A21,A23; then Ls.O in rng Lt by A21,A23,FUNCT_1:def 5; hence Ls.O c= Ls.O2 by A22,ZFMISC_1:92; end; thus for O2 holds X[O2] from Ordinal_Ind(A9,A10,A17); end; for x,y being set st x in rng Ls & y in rng Ls holds x,y are_c=-comparable proof let x,y be set; assume A24: x in rng Ls & y in rng Ls; then consider o1 being set such that A25: o1 in dom Ls & Ls.o1 = x by FUNCT_1:def 5; consider o2 being set such that A26: o2 in dom Ls & Ls.o2 = y by A24,FUNCT_1:def 5; reconsider o1' = o1, o2' = o2 as Ordinal by A25,A26,ORDINAL1:23; o1' c= o2' or o2' c= o1'; then x c= y or y c= x by A8,A25,A26; hence thesis by XBOOLE_0:def 9; end; then A27: rng Ls is c=-linear by ORDINAL1:def 9; rng Ls c= PFuncs(X,Y) proof let z be set; assume z in rng Ls; then consider o being set such that A28: o in dom Ls & z = Ls.o by FUNCT_1:def 5; reconsider o as Ordinal by A28,ORDINAL1:23; Ls.o = ConsecutiveDelta(q,o) by A5,A28; then reconsider h = Ls.o as BiFunction of ConsecutiveSet(A,o),L by A4,A5,A28; A29: dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):] by FUNCT_2:def 1; A30: rng h c= Y; o c= O1 by A5,A28,ORDINAL1:def 2; then ConsecutiveSet(A,o) c= ConsecutiveSet(A,O1) by Th32; then dom h c= X by A29,ZFMISC_1:119; hence z in PFuncs(X,Y) by A28,A30,PARTFUN1:def 5; end; then f in PFuncs(X,Y) by A27,HAHNBAN:13; then consider g being Function such that A31: f = g & dom g c= X & rng g c= Y by PARTFUN1:def 5; reconsider f as Function by A31; Ls is Function-yielding proof let x be set; assume A32: x in dom Ls; then reconsider o = x as Ordinal by ORDINAL1:23; Ls.o = ConsecutiveDelta(q,o) by A5,A32; hence Ls.x is Function by A4,A5,A32; end; then reconsider LsF = Ls as Function-yielding Function; A33: dom f = union rng doms LsF by Th1; reconsider o1 = O1 as non empty Ordinal by A4; set YY = { [:ConsecutiveSet(A,O2),ConsecutiveSet(A,O2):] where O2 is Element of o1 : not contradiction }; A34: rng doms Ls = YY proof thus rng doms Ls c= YY proof let Z be set; assume Z in rng doms Ls; then consider o being set such that A35: o in dom doms Ls & Z = (doms Ls).o by FUNCT_1:def 5; A36: o in dom LsF by A35,EXTENS_1:3; then reconsider o' = o as Element of o1 by A5; Ls.o' = ConsecutiveDelta(q,o') by A5; then reconsider ls = Ls.o' as BiFunction of ConsecutiveSet(A,o'),L by A4; Z = dom ls by A35,A36,FUNCT_6:31 .= [:ConsecutiveSet(A,o'),ConsecutiveSet(A,o'):] by FUNCT_2:def 1; hence Z in YY; end; let Z be set; assume Z in YY; then consider o being Element of o1 such that A37: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):]; o in dom LsF by A5; then A38: o in dom doms LsF by EXTENS_1:3; Ls.o = ConsecutiveDelta(q,o) by A5; then reconsider ls = Ls.o as BiFunction of ConsecutiveSet(A,o),L by A4; Z = dom ls by A37,FUNCT_2:def 1 .= (doms Ls).o by A5,FUNCT_6:31; hence Z in rng doms Ls by A38,FUNCT_1:def 5; end; {} in O1 by A4,ORDINAL3:10; then reconsider RTs = rng Ts as non empty set by A7,FUNCT_1:12; for x,y being set st x in RTs & y in RTs holds x,y are_c=-comparable proof let x,y be set; assume A39: x in RTs & y in RTs; then consider o1 being set such that A40: o1 in dom Ts & Ts.o1 = x by FUNCT_1:def 5; consider o2 being set such that A41: o2 in dom Ts & Ts.o2 = y by A39,FUNCT_1:def 5; reconsider o1' = o1, o2' = o2 as Ordinal by A40,A41,ORDINAL1:23; A42: Ts.o1' = ConsecutiveSet(A,o1') by A7,A40; A43: Ts.o2' = ConsecutiveSet(A,o2') by A7,A41; o1' c= o2' or o2' c= o1'; then x c= y or y c= x by A40,A41,A42,A43,Th32; hence thesis by XBOOLE_0:def 9; end; then A44: RTs is c=-linear by ORDINAL1:def 9; A45: YY = { [:a,a:] where a is Element of RTs : a in RTs } proof set XX = { [:a,a:] where a is Element of RTs : a in RTs }; thus YY c= XX proof let Z be set; assume Z in YY; then consider o being Element of o1 such that A46: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):]; Ts.o = ConsecutiveSet(A,o) by A7; then reconsider CoS = ConsecutiveSet(A,o) as Element of RTs by A7,FUNCT_1:def 5; Z = [:CoS,CoS:] by A46; hence Z in XX; end; let Z be set; assume Z in XX; then consider a being Element of RTs such that A47: Z = [:a,a:] & a in RTs; consider o being set such that A48: o in dom Ts & a = Ts.o by FUNCT_1:def 5; reconsider o' = o as Ordinal by A48,ORDINAL1:23; A49: a = ConsecutiveSet(A,o') by A7,A48; consider O being Element of o1 such that A50: O = o' by A7,A48; thus Z in YY by A47,A49,A50; end; X = [:union rng Ts, ConsecutiveSet(A,O1):] by A4,A7,Th26 .= [:union RTs, union RTs :] by A4,A7,Th26 .= dom f by A33,A34,A44,A45,Th3; hence ConsecutiveDelta(q,O1) is BiFunction of CS,L by A6,A31,FUNCT_2:def 1,RELSET_1:11; end; for O holds Y[O] from Ordinal_Ind(A1,A2,A3); hence thesis; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; redefine func ConsecutiveDelta(q,O) -> BiFunction of ConsecutiveSet(A,O),L; coherence by Th33; end; theorem Th34: for d be BiFunction of A,L for q being QuadrSeq of d holds d c= ConsecutiveDelta(q,O) proof let d be BiFunction of A,L; let q be QuadrSeq of d; defpred X[Ordinal] means d c= ConsecutiveDelta(q,$1); A1: X[{}] by Th29; A2: for O1 st X[O1] holds X[succ O1] proof let O1; assume A3: d c= ConsecutiveDelta(q,O1); ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1), ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16; then ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O1) by Th22; hence d c= ConsecutiveDelta(q,succ O1) by A3,XBOOLE_1:1; end; A4: for O2 st O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2] proof let O2; assume A5: O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds d c= ConsecutiveDelta(q,O1); deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Ls being T-Sequence such that A6: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1) from TS_Lambda; A7: ConsecutiveDelta(q,O2) = union rng Ls by A5,A6,Th31; A8: {} in O2 by A5,ORDINAL3:10; then Ls.{} = ConsecutiveDelta(q,{}) by A6 .= d by Th29; then d in rng Ls by A6,A8,FUNCT_1:def 5; hence d c= ConsecutiveDelta(q,O2) by A7,ZFMISC_1:92; end; for O holds X[O] from Ordinal_Ind(A1,A2,A4); hence thesis; end; theorem Th35: for d being BiFunction of A,L for q being QuadrSeq of d st O1 c= O2 holds ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2) proof let d be BiFunction of A,L; let q be QuadrSeq of d; defpred X[Ordinal] means O1 c= $1 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,$1); A1: X[{}] by XBOOLE_1:3; A2: for O2 st X[O2] holds X[succ O2] proof let O2; assume A3: O1 c= O2 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2); assume A4: O1 c= succ O2; per cases; suppose O1 = succ O2; hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O2); suppose O1 <> succ O2; then O1 c< succ O2 by A4,XBOOLE_0:def 8; then A5: O1 in succ O2 by ORDINAL1:21; ConsecutiveDelta(q,succ O2) = new_bi_fun(BiFun(ConsecutiveDelta(q,O2), ConsecutiveSet(A,O2),L),Quadr(q,O2)) by Th30 .= new_bi_fun(ConsecutiveDelta(q,O2),Quadr(q,O2)) by Def16; then ConsecutiveDelta(q,O2) c= ConsecutiveDelta(q,succ O2) by Th22; hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1; end; A6: for O2 st O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2] proof let O2; assume A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds O1 c= O3 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O3); assume A8: O1 c= O2; deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider L being T-Sequence such that A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3) from TS_Lambda; A10: ConsecutiveDelta(q,O2) = union rng L by A7,A9,Th31; per cases; suppose O1 = O2; hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2); suppose O1 <> O2; then O1 c< O2 by A8,XBOOLE_0:def 8; then A11: O1 in O2 by ORDINAL1:21; then A12: L.O1 = ConsecutiveDelta(q,O1) by A9; L.O1 in rng L by A9,A11,FUNCT_1:def 5; hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2) by A10,A12,ZFMISC_1:92; end; for O2 holds X[O2] from Ordinal_Ind(A1,A2,A6); hence thesis; end; theorem Th36: for d be BiFunction of A,L st d is zeroed for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is zeroed proof let d be BiFunction of A,L; assume A1: d is zeroed; let q be QuadrSeq of d; defpred X[Ordinal] means ConsecutiveDelta(q,$1) is zeroed; A2: X[{}] proof let z be Element of ConsecutiveSet(A,{}); reconsider z' = z as Element of A by Th24; thus ConsecutiveDelta(q,{}).(z,z) = d.(z',z') by Th29 .= Bottom L by A1,Def7 ; end; A3: for O1 st X[O1] holds X[succ O1] proof let O1; assume ConsecutiveDelta(q,O1) is zeroed; then A4:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is zeroed by Th18; let z be Element of ConsecutiveSet(A,succ O1); reconsider z' = z as Element of new_set ConsecutiveSet(A,O1) by Th25; ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1), ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16; hence ConsecutiveDelta(q,succ O1).(z,z) = new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)).(z',z') .= Bottom L by A4,Def7; end; A5: for O2 st O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2] proof let O2; assume A6: O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is zeroed; deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Ls being T-Sequence such that A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1) from TS_Lambda; A8: ConsecutiveDelta(q,O2) = union rng Ls by A6,A7,Th31; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ts being T-Sequence such that A9: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1) from TS_Lambda; A10: ConsecutiveSet(A,O2) = union rng Ts by A6,A9,Th26; set CS = ConsecutiveSet(A,O2); reconsider f = union rng Ls as BiFunction of CS,L by A8; f is zeroed proof let x be Element of CS; consider y being set such that A11: x in y & y in rng Ts by A10,TARSKI:def 4; consider o being set such that A12: o in dom Ts & y = Ts.o by A11,FUNCT_1:def 5; reconsider o as Ordinal by A12,ORDINAL1:23; A13: x in ConsecutiveSet(A,o) by A9,A11,A12; A14: Ls.o = ConsecutiveDelta(q,o) by A7,A9,A12; then reconsider h = Ls.o as BiFunction of ConsecutiveSet(A,o),L; A15: h is zeroed proof let z be Element of ConsecutiveSet(A,o); A16: ConsecutiveDelta(q,o) is zeroed by A6,A9,A12; thus h.(z,z) = ConsecutiveDelta(q,o).(z,z) by A7,A9,A12 .= Bottom L by A16,Def7; end; ConsecutiveDelta(q,o) in rng Ls by A7,A9,A12,A14,FUNCT_1:def 5; then A17: h c= f by A14,ZFMISC_1:92; reconsider x' = x as Element of ConsecutiveSet(A,o) by A9,A11,A12; dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):] by FUNCT_2:def 1; then A18: [x,x] in dom h by A13,ZFMISC_1:106; thus f.(x,x) = f.[x,x] by BINOP_1:def 1 .= h.[x,x] by A17,A18,GRFUNC_1:8 .= h.(x',x') by BINOP_1:def 1 .= Bottom L by A15,Def7; end; hence ConsecutiveDelta(q,O2) is zeroed by A6,A7,Th31; end; for O holds X[O] from Ordinal_Ind(A2,A3,A5); hence thesis; end; theorem Th37: for d be BiFunction of A,L st d is symmetric for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is symmetric proof let d be BiFunction of A,L; assume A1: d is symmetric; let q be QuadrSeq of d; defpred X[Ordinal] means ConsecutiveDelta(q,$1) is symmetric; A2: X[{}] proof let x,y be Element of ConsecutiveSet(A,{}); reconsider x' = x, y' = y as Element of A by Th24; thus ConsecutiveDelta(q,{}).(x,y) = d.(x',y') by Th29 .= d.(y',x') by A1,Def6 .= ConsecutiveDelta(q,{}).(y,x) by Th29; end; A3: for O1 st X[O1] holds X[succ O1] proof let O1; assume ConsecutiveDelta(q,O1) is symmetric; then A4:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is symmetric by Th19; let x,y be Element of ConsecutiveSet(A,succ O1); reconsider x'=x, y'=y as Element of new_set ConsecutiveSet(A,O1) by Th25; A5:ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1), ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16; hence ConsecutiveDelta(q,succ O1).(x,y) = new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)).(y',x') by A4,Def6 .= ConsecutiveDelta(q,succ O1).(y,x) by A5; end; A6: for O2 st O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2] proof let O2; assume A7: O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is symmetric; deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Ls being T-Sequence such that A8: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1) from TS_Lambda; A9: ConsecutiveDelta(q,O2) = union rng Ls by A7,A8,Th31; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ts being T-Sequence such that A10: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1) from TS_Lambda; A11: ConsecutiveSet(A,O2) = union rng Ts by A7,A10,Th26; set CS = ConsecutiveSet(A,O2); reconsider f = union rng Ls as BiFunction of CS,L by A9; f is symmetric proof let x,y be Element of CS; consider x1 being set such that A12: x in x1 & x1 in rng Ts by A11,TARSKI:def 4; consider o1 being set such that A13: o1 in dom Ts & x1 = Ts.o1 by A12,FUNCT_1:def 5; consider y1 being set such that A14: y in y1 & y1 in rng Ts by A11,TARSKI:def 4; consider o2 being set such that A15: o2 in dom Ts & y1 = Ts.o2 by A14,FUNCT_1:def 5; reconsider o1,o2 as Ordinal by A13,A15,ORDINAL1:23; A16: x in ConsecutiveSet(A,o1) by A10,A12,A13; A17: y in ConsecutiveSet(A,o2) by A10,A14,A15; A18: Ls.o1 = ConsecutiveDelta(q,o1) by A8,A10,A13; then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L; A19: h1 is symmetric proof let x,y be Element of ConsecutiveSet(A,o1); A20: ConsecutiveDelta(q,o1) is symmetric by A7,A10,A13; thus h1.(x,y) = ConsecutiveDelta(q,o1).(x,y) by A8,A10,A13 .= ConsecutiveDelta(q,o1).(y,x) by A20,Def6 .= h1.(y,x) by A8,A10,A13; end; A21: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):] by FUNCT_2:def 1; A22: Ls.o2 = ConsecutiveDelta(q,o2) by A8,A10,A15; then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet(A,o2),L; A23: h2 is symmetric proof let x,y be Element of ConsecutiveSet(A,o2); A24: ConsecutiveDelta(q,o2) is symmetric by A7,A10,A15; thus h2.(x,y) = ConsecutiveDelta(q,o2).(x,y) by A8,A10,A15 .= ConsecutiveDelta(q,o2).(y,x) by A24,Def6 .= h2.(y,x) by A8,A10,A15; end; A25: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):] by FUNCT_2:def 1; per cases; suppose o1 c= o2; then A26: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by Th32; then reconsider x'=x, y'=y as Element of ConsecutiveSet(A,o2) by A10,A14,A15,A16; ConsecutiveDelta(q,o2) in rng Ls by A8,A10,A15,A22,FUNCT_1:def 5 ; then A27: h2 c= f by A22,ZFMISC_1:92; A28: [x,y] in dom h2 & [y,x] in dom h2 by A16,A17,A25,A26,ZFMISC_1:106; thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h2.[x,y] by A27,A28,GRFUNC_1:8 .= h2.(x',y') by BINOP_1:def 1 .= h2.(y',x') by A23,Def6 .= h2.[y,x] by BINOP_1:def 1 .= f.[y,x] by A27,A28,GRFUNC_1:8 .= f.(y,x) by BINOP_1:def 1; suppose o2 c= o1; then A29: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by Th32; then reconsider x'=x, y'=y as Element of ConsecutiveSet(A,o1) by A10,A12,A13,A17; ConsecutiveDelta(q,o1) in rng Ls by A8,A10,A13,A18,FUNCT_1:def 5 ; then A30: h1 c= f by A18,ZFMISC_1:92; A31: [x,y] in dom h1 & [y,x] in dom h1 by A16,A17,A21,A29,ZFMISC_1:106; thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h1.[x,y] by A30,A31,GRFUNC_1:8 .= h1.(x',y') by BINOP_1:def 1 .= h1.(y',x') by A19,Def6 .= h1.[y,x] by BINOP_1:def 1 .= f.[y,x] by A30,A31,GRFUNC_1:8 .= f.(y,x) by BINOP_1:def 1; end; hence ConsecutiveDelta(q,O2) is symmetric by A7,A8,Th31; end; for O holds X[O] from Ordinal_Ind(A2,A3,A6); hence thesis; end; theorem Th38: for d be BiFunction of A,L st d is symmetric u.t.i. for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta(q,O) is u.t.i. proof let d be BiFunction of A,L; assume that A1: d is symmetric and A2: d is u.t.i.; let q be QuadrSeq of d; defpred X[Ordinal] means $1 c= DistEsti(d) implies ConsecutiveDelta(q,$1) is u.t.i.; A3: X[{}] proof assume {} c= DistEsti(d); let x,y,z be Element of ConsecutiveSet(A,{}); reconsider x' = x, y' = y, z' = z as Element of A by Th24; A4:ConsecutiveDelta(q,{}) = d by Th29; d.(x',z') <= d.(x',y') "\/" d.(y',z') by A2,Def8; hence ConsecutiveDelta(q,{}).(x,z) <= ConsecutiveDelta(q,{}).(x,y) "\/" ConsecutiveDelta(q,{}).(y,z) by A4; end; A5: for O1 st X[O1] holds X[succ O1] proof let O1; assume that A6: O1 c= DistEsti(d) implies ConsecutiveDelta(q,O1) is u.t.i. and A7: succ O1 c= DistEsti(d); A8: O1 in DistEsti(d) by A7,ORDINAL1:33; A9: ConsecutiveDelta(q,O1) is symmetric by A1,Th37; let x,y,z be Element of ConsecutiveSet(A,succ O1); set f = new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)); reconsider x' = x, y' = y, z' = z as Element of new_set ConsecutiveSet(A,O1) by Th25; A10: O1 in dom q by A8,Th28; then q.O1 in rng q by FUNCT_1:def 5; then q.O1 in {[u,v,a',b'] where u is Element of A, v is Element of A, a' is Element of L, b' is Element of L: d.(u,v) <= a'"\/"b'} by Def14; then consider u,v be Element of A, a',b' be Element of L such that A11: q.O1 = [u,v,a',b'] & d.(u,v) <= a'"\/"b'; set X = Quadr(q,O1)`1, Y = Quadr(q,O1)`2; reconsider a = Quadr(q,O1)`3, b = Quadr(q,O1)`4 as Element of L ; A12: Quadr(q,O1) = [u,v,a',b'] by A10,A11,Def15; then A13: u = X by MCART_1:def 8; A14: v = Y by A12,MCART_1:def 9; A15: a' = a by A12,MCART_1:def 10; A16: b' = b by A12,MCART_1:def 11; A17: dom d = [:A,A:] by FUNCT_2:def 1; A18: d c= ConsecutiveDelta(q,O1) by Th34; d.(u,v) = d.[u,v] by BINOP_1:def 1 .= ConsecutiveDelta(q,O1).[X,Y] by A13,A14,A17,A18,GRFUNC_1:8 .= ConsecutiveDelta(q,O1).(X,Y) by BINOP_1:def 1; then A19:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is u.t.i. by A6,A8,A9,A11,A15,A16,Th20,ORDINAL1:def 2; A20: ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1), ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16; f.(x',z') <= f.(x',y') "\/" f.(y',z') by A19,Def8; hence ConsecutiveDelta(q,succ O1).(x,z) <= ConsecutiveDelta(q,succ O1).(x,y) "\/" ConsecutiveDelta(q,succ O1).(y,z) by A20; end; A21: for O2 st O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2] proof let O2; assume that A22: O2 <> {} & O2 is_limit_ordinal & for O1 st O1 in O2 holds (O1 c= DistEsti(d) implies ConsecutiveDelta(q,O1) is u.t.i.) and A23: O2 c= DistEsti(d); deffunc U(Ordinal) = ConsecutiveDelta(q,$1); consider Ls being T-Sequence such that A24: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1) from TS_Lambda; A25: ConsecutiveDelta(q,O2) = union rng Ls by A22,A24,Th31; deffunc U(Ordinal) = ConsecutiveSet(A,$1); consider Ts being T-Sequence such that A26: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1) from TS_Lambda; A27: ConsecutiveSet(A,O2) = union rng Ts by A22,A26,Th26; set CS = ConsecutiveSet(A,O2); reconsider f = union rng Ls as BiFunction of CS,L by A25; f is u.t.i. proof let x,y,z be Element of CS; consider X being set such that A28: x in X & X in rng Ts by A27,TARSKI:def 4; consider o1 being set such that A29: o1 in dom Ts & X = Ts.o1 by A28,FUNCT_1:def 5; consider Y being set such that A30: y in Y & Y in rng Ts by A27,TARSKI:def 4; consider o2 being set such that A31: o2 in dom Ts & Y = Ts.o2 by A30,FUNCT_1:def 5; consider Z being set such that A32: z in Z & Z in rng Ts by A27,TARSKI:def 4; consider o3 being set such that A33: o3 in dom Ts & Z = Ts.o3 by A32,FUNCT_1:def 5; reconsider o1,o2,o3 as Ordinal by A29,A31,A33,ORDINAL1:23; A34: x in ConsecutiveSet(A,o1) by A26,A28,A29; A35: y in ConsecutiveSet(A,o2) by A26,A30,A31; A36: z in ConsecutiveSet(A,o3) by A26,A32,A33; A37: Ls.o1 = ConsecutiveDelta(q,o1) by A24,A26,A29; then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L; A38: h1 is u.t.i. proof let x,y,z be Element of ConsecutiveSet(A,o1); A39:ConsecutiveDelta(q,o1) = h1 by A24,A26,A29; o1 c= DistEsti(d) by A23,A26,A29,ORDINAL1:def 2; then ConsecutiveDelta(q,o1) is u.t.i. by A22,A26,A29; hence h1.(x,z) <= h1.(x,y) "\/" h1.(y,z) by A39,Def8; end; A40: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):] by FUNCT_2:def 1; A41: Ls.o2 = ConsecutiveDelta(q,o2) by A24,A26,A31; then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet(A,o2),L; A42: h2 is u.t.i. proof let x,y,z be Element of ConsecutiveSet(A,o2); A43:ConsecutiveDelta(q,o2) = h2 by A24,A26,A31; o2 c= DistEsti(d) by A23,A26,A31,ORDINAL1:def 2; then ConsecutiveDelta(q,o2) is u.t.i. by A22,A26,A31; hence h2.(x,z) <= h2.(x,y) "\/" h2.(y,z) by A43,Def8; end; A44: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):] by FUNCT_2:def 1; A45: Ls.o3 = ConsecutiveDelta(q,o3) by A24,A26,A33; then reconsider h3 = Ls.o3 as BiFunction of ConsecutiveSet(A,o3),L; A46: h3 is u.t.i. proof let x,y,z be Element of ConsecutiveSet(A,o3); A47:ConsecutiveDelta(q,o3) = h3 by A24,A26,A33; o3 c= DistEsti(d) by A23,A26,A33,ORDINAL1:def 2; then ConsecutiveDelta(q,o3) is u.t.i. by A22,A26,A33; hence h3.(x,z) <= h3.(x,y) "\/" h3.(y,z) by A47,Def8; end; A48: dom h3 = [:ConsecutiveSet(A,o3),ConsecutiveSet(A,o3):] by FUNCT_2:def 1; per cases; suppose A49: o1 c= o3; then A50: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by Th32; thus f.(x,y) "\/" f.(y,z) >= f.(x,z) proof per cases; suppose o2 c= o3; then A51: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o3) by Th32; then reconsider y' = y as Element of ConsecutiveSet(A,o3) by A35; reconsider x' = x as Element of ConsecutiveSet(A,o3) by A34,A50; reconsider z' = z as Element of ConsecutiveSet(A,o3) by A26,A32,A33; ConsecutiveDelta(q,o3) in rng Ls by A24,A26,A33,A45,FUNCT_1:def 5 ; then A52: h3 c= f by A45,ZFMISC_1:92; A53: [x,y] in dom h3 by A34,A35,A48,A50,A51,ZFMISC_1:106; A54: [y,z] in dom h3 by A35,A36,A48,A51,ZFMISC_1:106; A55: [x,z] in dom h3 by A34,A36,A48,A50,ZFMISC_1:106; A56: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h3.[x,y] by A52,A53,GRFUNC_1:8 .= h3.(x',y') by BINOP_1:def 1; A57: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h3.[y,z] by A52,A54,GRFUNC_1:8 .= h3.(y',z') by BINOP_1:def 1; f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h3.[x,z] by A52,A55,GRFUNC_1:8 .= h3.(x',z') by BINOP_1:def 1; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A46,A56,A57,Def8; suppose o3 c= o2; then A58: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by Th32; then reconsider z' = z as Element of ConsecutiveSet(A,o2) by A36; ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by A49,Th32; then A59: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by A58,XBOOLE_1:1; then reconsider x' = x as Element of ConsecutiveSet(A,o2) by A34; reconsider y' = y as Element of ConsecutiveSet(A,o2) by A26,A30,A31; ConsecutiveDelta(q,o2) in rng Ls by A24,A26,A31,A41,FUNCT_1:def 5 ; then A60: h2 c= f by A41,ZFMISC_1:92; A61: [x,y] in dom h2 by A34,A35,A44,A59,ZFMISC_1:106; A62: [y,z] in dom h2 by A35,A36,A44,A58,ZFMISC_1:106; A63: [x,z] in dom h2 by A34,A36,A44,A58,A59,ZFMISC_1:106; A64: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h2.[x,y] by A60,A61,GRFUNC_1:8 .= h2.(x',y') by BINOP_1:def 1; A65: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h2.[y,z] by A60,A62,GRFUNC_1:8 .= h2.(y',z') by BINOP_1:def 1; f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h2.[x,z] by A60,A63,GRFUNC_1:8 .= h2.(x',z') by BINOP_1:def 1; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A42,A64,A65,Def8; end; suppose A66: o3 c= o1; then A67: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by Th32; thus f.(x,y) "\/" f.(y,z) >= f.(x,z) proof per cases; suppose o1 c= o2; then A68: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by Th32; then reconsider x' = x as Element of ConsecutiveSet(A,o2) by A34; ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by A66,Th32; then A69: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by A68,XBOOLE_1:1; then reconsider z' = z as Element of ConsecutiveSet(A,o2) by A36; reconsider y' = y as Element of ConsecutiveSet(A,o2) by A26,A30,A31; ConsecutiveDelta(q,o2) in rng Ls by A24,A26,A31,A41,FUNCT_1:def 5 ; then A70: h2 c= f by A41,ZFMISC_1:92; A71: [x,y] in dom h2 by A34,A35,A44,A68,ZFMISC_1:106; A72: [y,z] in dom h2 by A35,A36,A44,A69,ZFMISC_1:106; A73: [x,z] in dom h2 by A34,A36,A44,A68,A69,ZFMISC_1:106; A74: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h2.[x,y] by A70,A71,GRFUNC_1:8 .= h2.(x',y') by BINOP_1:def 1; A75: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h2.[y,z] by A70,A72,GRFUNC_1:8 .= h2.(y',z') by BINOP_1:def 1; f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h2.[x,z] by A70,A73,GRFUNC_1:8 .= h2.(x',z') by BINOP_1:def 1; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A42,A74,A75,Def8; suppose o2 c= o1; then A76: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by Th32; then reconsider y' = y as Element of ConsecutiveSet(A,o1) by A35; reconsider z' = z as Element of ConsecutiveSet(A,o1) by A36,A67; reconsider x' = x as Element of ConsecutiveSet(A,o1) by A26,A28,A29; ConsecutiveDelta(q,o1) in rng Ls by A24,A26,A29,A37,FUNCT_1:def 5 ; then A77: h1 c= f by A37,ZFMISC_1:92; A78: [x,y] in dom h1 by A34,A35,A40,A76,ZFMISC_1:106; A79: [y,z] in dom h1 by A35,A36,A40,A67,A76,ZFMISC_1:106; A80: [x,z] in dom h1 by A34,A36,A40,A67,ZFMISC_1:106; A81: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h1.[x,y] by A77,A78,GRFUNC_1:8 .= h1.(x',y') by BINOP_1:def 1; A82: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h1.[y,z] by A77,A79,GRFUNC_1:8 .= h1.(y',z') by BINOP_1:def 1; f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h1.[x,z] by A77,A80,GRFUNC_1:8 .= h1.(x',z') by BINOP_1:def 1; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A38,A81,A82,Def8; end; end; hence ConsecutiveDelta(q,O2) is u.t.i. by A22,A24,Th31; end; for O holds X[O] from Ordinal_Ind(A3,A5,A21); hence thesis; end; theorem for d being distance_function of A,L for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta(q,O) is distance_function of ConsecutiveSet(A,O),L by Th36,Th37,Th38; definition let A,L; let d be BiFunction of A,L; func NextSet(d) equals :Def18: ConsecutiveSet(A,DistEsti(d)); correctness; end; definition let A,L; let d be BiFunction of A,L; cluster NextSet(d) -> non empty; coherence proof ConsecutiveSet(A,DistEsti(d)) is non empty; hence thesis by Def18; end; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; func NextDelta(q) equals :Def19: ConsecutiveDelta(q,DistEsti(d)); correctness; end; definition let A,L; let d be distance_function of A,L; let q be QuadrSeq of d; redefine func NextDelta(q) -> distance_function of NextSet(d),L; coherence proof A1: ConsecutiveDelta(q,DistEsti(d)) = NextDelta(q) by Def19; ConsecutiveSet(A,DistEsti(d)) = NextSet(d) by Def18; hence NextDelta(q) is distance_function of NextSet(d),L by A1,Th36,Th37,Th38; end; end; definition let A,L; let d be distance_function of A,L; let Aq be non empty set, dq be distance_function of Aq,L; pred Aq, dq is_extension_of A,d means :Def20: ex q being QuadrSeq of d st Aq = NextSet(d) & dq = NextDelta(q); end; theorem Th40: for d be distance_function of A,L for Aq be non empty set, dq be distance_function of Aq,L st Aq, dq is_extension_of A,d for x,y being Element of A, a,b being Element of L st d.(x,y) <= a "\/" b ex z1,z2,z3 being Element of Aq st dq.(x,z1) = a & dq.(z2,z3) = a & dq.(z1,z2) = b & dq.(z3,y) = b proof let d be distance_function of A,L; let Aq be non empty set, dq be distance_function of Aq,L; assume Aq, dq is_extension_of A,d; then consider q being QuadrSeq of d such that A1: Aq = NextSet(d) and A2: dq = NextDelta(q) by Def20; let x,y be Element of A; let a,b be Element of L; assume A3: d.(x,y) <= a "\/" b; rng q = {[x',y',a',b'] where x' is Element of A, y' is Element of A, a' is Element of L, b' is Element of L: d.(x',y') <= a'"\/"b'} by Def14; then [x,y,a,b] in rng q by A3; then consider o being set such that A4: o in dom q & q.o = [x,y,a,b] by FUNCT_1:def 5; reconsider o as Ordinal by A4,ORDINAL1:23; A5: q.o = Quadr(q,o) by A4,Def15; then A6: x = Quadr(q,o)`1 by A4,MCART_1:78; A7: y = Quadr(q,o)`2 by A4,A5,MCART_1:78; A8: a = Quadr(q,o)`3 by A4,A5,MCART_1:78; A9: b = Quadr(q,o)`4 by A4,A5,MCART_1:78; reconsider B = ConsecutiveSet(A,o) as non empty set; reconsider Q = Quadr(q,o) as Element of [:B,B,the carrier of L,the carrier of L:]; reconsider cd = ConsecutiveDelta(q,o) as BiFunction of B,L; x in A & y in A & A c= B by Th27; then reconsider xo = x, yo = y as Element of B; xo in B & yo in B & B c= new_set B by Th21; then reconsider x1 = xo, y1 = yo as Element of new_set B; A10: ConsecutiveSet(A,succ o) = new_set B by Th25; o in DistEsti(d) by A4,Th28; then A11: succ o c= DistEsti(d) by ORDINAL1:33; then A12: ConsecutiveDelta(q,succ o) c= ConsecutiveDelta(q,DistEsti(d)) by Th35 ; ConsecutiveDelta(q,succ o) = new_bi_fun(BiFun(ConsecutiveDelta(q,o), ConsecutiveSet(A,o),L),Quadr(q,o)) by Th30 .= new_bi_fun(cd,Q) by Def16; then A13: new_bi_fun(cd,Q) c= dq by A2,A12,Def19; {B} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14; then {B} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2; then A14: {B} in new_set B by Def10; {{B}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14; then {{B}} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2; then A15: {{B}} in new_set B by Def10; {{{B}}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14; then {{{B}}} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2; then A16: {{{B}}} in new_set B by Def10; A17: cd is zeroed by Th36; A18: dom new_bi_fun(cd,Q) = [:new_set B,new_set B:] by FUNCT_2:def 1; then A19: [x1,{B}] in dom new_bi_fun(cd,Q) by A14,ZFMISC_1:106; A20: [{{B}},{{{B}}}] in dom new_bi_fun(cd,Q) by A15,A16,A18,ZFMISC_1:106; A21: [{B},{{B}}] in dom new_bi_fun(cd,Q) by A14,A15,A18,ZFMISC_1:106; A22: [{{{B}}},y1] in dom new_bi_fun(cd,Q) by A16,A18,ZFMISC_1:106; new_set B c= ConsecutiveSet(A,DistEsti(d)) by A10,A11,Th32; then reconsider z1={B},z2={{B}},z3={{{B}}} as Element of Aq by A1,A14,A15, A16,Def18; take z1,z2,z3; thus dq.(x,z1) = dq.[x,z1] by BINOP_1:def 1 .= new_bi_fun(cd,Q).[x1,{B}] by A13,A19,GRFUNC_1:8 .= new_bi_fun(cd,Q).(x1,{B}) by BINOP_1:def 1 .= cd.(xo,xo)"\/"a by A6,A8,Def11 .= Bottom L"\/" a by A17,Def7 .= a by WAYBEL_1:4; thus dq.(z2,z3) = dq.[z2,z3] by BINOP_1:def 1 .= new_bi_fun(cd,Q).[{{B}},{{{B}}}] by A13,A20,GRFUNC_1:8 .= new_bi_fun(cd,Q).({{B}},{{{B}}}) by BINOP_1:def 1 .= a by A8,Def11; thus dq.(z1,z2) = dq.[z1,z2] by BINOP_1:def 1 .= new_bi_fun(cd,Q).[{B},{{B}}] by A13,A21,GRFUNC_1:8 .= new_bi_fun(cd,Q).({B},{{B}}) by BINOP_1:def 1 .= b by A9,Def11; thus dq.(z3,y) = dq.[z3,y] by BINOP_1:def 1 .= new_bi_fun(cd,Q).[{{{B}}},y1] by A13,A22,GRFUNC_1:8 .= new_bi_fun(cd,Q).({{{B}}},y1) by BINOP_1:def 1 .= cd.(yo,yo)"\/"b by A7,A9,Def11 .= Bottom L"\/" b by A17,Def7 .= b by WAYBEL_1:4; end; definition let A,L; let d be distance_function of A,L; mode ExtensionSeq of A,d -> Function means :Def21: dom it = NAT & it.0 = [A,d] & for n being Nat holds ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & it.n = [A',d'] & it.(n+1) = [Aq,dq]; existence proof defpred P[set,set,set] means (ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & $2 = [A',d'] & $3 = [Aq,dq]) or $3= 0 & not ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & $2 = [A',d']; A1: for n being Nat for x being set ex y being set st P[n,x,y] proof let n be Nat; let x be set; per cases; suppose ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & x = [A',d']; then consider A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L such that A2: Aq, dq is_extension_of A',d' and A3: x = [A',d']; take [Aq,dq]; thus thesis by A2,A3; suppose A4: not ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & x = [A',d']; take 0; thus thesis by A4; end; consider f being Function such that A5: dom f = NAT and A6: f.0 = [A,d] and A7: for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecChoice(A1); take f; thus dom f = NAT by A5; thus f.0 = [A,d] by A6; defpred X[Nat] means ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & f.$1 = [A',d'] & f.($1+1) = [Aq,dq]; ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A',d' & f.0 = [A',d'] proof take A,d; consider q being QuadrSeq of d; set Aq = NextSet(d); consider dq being distance_function of Aq,L such that A8: dq = NextDelta(q); take Aq,dq; thus Aq, dq is_extension_of A,d by A8,Def20; thus f.0 = [A,d] by A6; end; then A9: X[0] by A7; A10: for k being Nat st X[k] holds X[k+1] proof let k be Nat; given A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L such that Aq, dq is_extension_of A',d' and f.k = [A',d'] and A11: f.(k+1) = [Aq,dq]; ex A1 being non empty set, d1 being distance_function of A1,L, AQ being non empty set, DQ being distance_function of AQ,L st AQ, DQ is_extension_of A1,d1 & f.(k+1) = [A1,d1] proof take Aq,dq; set AQ = NextSet(dq); consider Q being QuadrSeq of dq; set DQ = NextDelta(Q); take AQ,DQ; thus AQ, DQ is_extension_of Aq,dq by Def20; thus f.(k+1) = [Aq,dq] by A11; end; hence thesis by A7; end; thus for k being Nat holds X[k] from Ind(A9,A10); end; end; theorem Th41: for d be distance_function of A,L for S being ExtensionSeq of A,d for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1 proof let d be distance_function of A,L; let S be ExtensionSeq of A,d; let k be Nat; defpred X[Nat] means k <= $1 implies (S.k)`1 c= (S.$1)`1; A1: X[0] by NAT_1:19; A2: for i being Nat st X[i] holds X[i+1] proof let i be Nat; assume that A3: k <= i implies (S.k)`1 c= (S.i)`1 and A4: k <= i+1; per cases by A4,NAT_1:26; suppose k = i+1; hence (S.k)`1 c= (S.(i+1))`1; suppose A5: k <= i; consider A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L such that A6: Aq, dq is_extension_of A',d' and A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def21; consider q being QuadrSeq of d' such that A8: Aq = NextSet(d') and dq = NextDelta(q) by A6,Def20; A9: (S.i)`1 = A' by A7,MCART_1:def 1; A10: (S.(i+1))`1 = NextSet(d') by A7,A8,MCART_1:def 1 .= ConsecutiveSet(A',DistEsti(d')) by Def18; (S.i)`1 c= ConsecutiveSet(A',DistEsti(d')) by A9,Th27; hence (S.k)`1 c= (S.(i+1))`1 by A3,A5,A10,XBOOLE_1:1; end; thus for l being Nat holds X[l] from Ind(A1,A2); end; theorem Th42: for d be distance_function of A,L for S being ExtensionSeq of A,d for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2 proof let d be distance_function of A,L; let S be ExtensionSeq of A,d; let k be Nat; defpred X[Nat] means k <= $1 implies (S.k)`2 c= (S.$1)`2; A1: X[0] by NAT_1:19; A2: for i being Nat st X[i] holds X[i+1] proof let i be Nat; assume that A3: k <= i implies (S.k)`2 c= (S.i)`2 and A4: k <= i+1; per cases by A4,NAT_1:26; suppose k = i+1; hence (S.k)`2 c= (S.(i+1))`2; suppose A5: k <= i; consider A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L such that A6: Aq, dq is_extension_of A',d' and A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def21; consider q being QuadrSeq of d' such that Aq = NextSet(d') and A8: dq = NextDelta(q) by A6,Def20; A9: (S.i)`2 = d' by A7,MCART_1:def 2; A10: (S.(i+1))`2 = NextDelta(q) by A7,A8,MCART_1:def 2 .= ConsecutiveDelta(q,DistEsti(d')) by Def19; (S.i)`2 c= ConsecutiveDelta(q,DistEsti(d')) by A9,Th34; hence (S.k)`2 c= (S.(i+1))`2 by A3,A5,A10,XBOOLE_1:1; end; thus for l being Nat holds X[l] from Ind(A1,A2); end; definition let L; func BasicDF(L) -> distance_function of the carrier of L,L means :Def22: for x,y being Element of L holds (x <> y implies it.(x,y) = x"\/"y) & (x = y implies it.(x,y) = Bottom L); existence proof set A = the carrier of L; defpred X[Element of L,Element of L,set] means ($1 = $2 implies $3 = Bottom L) & ($1 <> $2 implies $3 = $1"\/"$2); A1: for x,y being Element of L ex z being Element of L st X[x,y,z] proof let x,y be Element of L; per cases; suppose A2: x = y; take Bottom L; thus thesis by A2; suppose A3: x <> y; take x"\/"y; thus thesis by A3; end; consider f being Function of [:the carrier of L,the carrier of L:],the carrier of L such that A4: for x,y being Element of L holds X[x,y,f.[x,y]] from FuncEx2D(A1); A5:for x,y being Element of L holds (x <> y implies f.(x,y) = x"\/"y) & (x = y implies f.(x,y) = Bottom L) proof let x,y be Element of L; thus x <> y implies f.(x,y) = x"\/"y proof assume A6: x <> y; thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= x"\/"y by A4,A6; end; thus x = y implies f.(x,y) = Bottom L proof assume A7: x = y; thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= Bottom L by A4,A7; end; end; reconsider f as BiFunction of A,L; A8: f is zeroed proof let x be Element of A; thus f.(x,x) = Bottom L by A5; end; A9: f is symmetric proof let x,y be Element of A; reconsider x' = x, y' = y as Element of L; per cases; suppose x = y; hence f.(x,y) = f.(y,x); suppose A10: x <> y; hence f.(x,y) = y' "\/" x' by A5 .= f.(y,x) by A5,A10; end; f is u.t.i. proof let x,y,z be Element of A; reconsider x' = x, y' = y, z' = z as Element of L; per cases; suppose A11: x = z; f.(x,y) "\/" f.(y,z) >= Bottom L by YELLOW_0:44; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A11; suppose A12: x <> z; thus f.(x,y) "\/" f.(y,z) >= f.(x,z) proof per cases; suppose A13: x = y; x' "\/" z' >= x' "\/" z' by ORDERS_1:24; then f.(x,z) >= x' "\/" z' by A5,A12; then Bottom L "\/" f.(x,z) >= x' "\/" z' by WAYBEL_1:4; then f.(x,y) "\/" f.(y,z) >= x' "\/" z' by A5,A13; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A12; suppose A14: x <> y; (x' "\/" y') "\/" f.(y,z) >= x' "\/" z' proof per cases; suppose A15: y = z; (x' "\/" y') >= x' "\/" y' by ORDERS_1:24; then Bottom L "\/" (x' "\/" y') >= x' "\/" z' by A15,WAYBEL_1:4 ; hence (x' "\/" y') "\/" f.(y,z) >= x' "\/" z' by A5,A15; suppose A16: y <> z; (x' "\/" z') "\/" y' = (x' "\/" z') "\/" (y' "\/" y') by YELLOW_5 :1 .= x' "\/" (z' "\/" (y' "\/" y')) by LATTICE3:14 .= x' "\/" (y' "\/" (y' "\/" z')) by LATTICE3:14 .= (x' "\/" y') "\/" (y' "\/" z') by LATTICE3:14; then (x' "\/" y') "\/" (y' "\/" z') >= x' "\/" z' by YELLOW_0:22; hence (x' "\/" y') "\/" f.(y,z) >= x' "\/" z' by A5,A16; end; then f.(x,y) "\/" f.(y,z) >= x' "\/" z' by A5,A14; hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A12; end; end; then reconsider f as distance_function of A,L by A8,A9; take f; thus thesis by A5; end; uniqueness proof let f1,f2 be distance_function of the carrier of L,L such that A17: for x,y being Element of L holds (x <> y implies f1.(x,y) = x"\/"y) & (x = y implies f1.(x,y) = Bottom L) and A18: for x,y being Element of L holds (x <> y implies f2.(x,y) = x"\/"y) & (x = y implies f2.(x,y) = Bottom L); A19: dom f1 = [:the carrier of L,the carrier of L:] by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; for z being set st z in dom f1 holds f1.z = f2.z proof let z be set; assume A20: z in dom f1; then consider x,y being set such that A21: z = [x,y] by ZFMISC_1:102; reconsider x,y as Element of L by A20,A21,ZFMISC_1:106; per cases; suppose A22: x = y; thus f1.z = f1.(x,y) by A21,BINOP_1:def 1 .= Bottom L by A17,A22 .= f2.(x,y) by A18,A22 .= f2.z by A21,BINOP_1:def 1; suppose A23: x <> y; thus f1.z = f1.(x,y) by A21,BINOP_1:def 1 .= x"\/"y by A17,A23 .= f2.(x,y) by A18,A23 .= f2.z by A21,BINOP_1:def 1; end; hence f1 = f2 by A19,FUNCT_1:9; end; end; theorem Th43: BasicDF(L) is onto proof set X = the carrier of L, f = BasicDF(L); for w being set st w in X ex z being set st z in [:X,X:] & w = f.z proof let w be set; assume A1: w in X; then reconsider w' = w as Element of L; reconsider w'' = w as Element of L by A1; per cases; suppose A2: w = Bottom L; take z = [w,w]; thus z in [:X,X:] by A1,ZFMISC_1:106; thus f.z = f.(w',w') by BINOP_1:def 1.= w by A2,Def22; suppose A3: w <> Bottom L; take z = [Bottom L,w]; thus z in [:X,X:] by A1,ZFMISC_1:106; thus f.z = f.(Bottom L,w') by BINOP_1:def 1 .= Bottom L "\/" w'' by A3,Def22 .= w by WAYBEL_1:4; end; then rng f = the carrier of L by FUNCT_2:16; hence BasicDF(L) is onto by FUNCT_2:def 3; end; Lm2: now let j be Nat; assume A1: 1 <= j & j < 5; then j < 4+1; then j <= 4 by NAT_1:38; then j = 0 or j = 1 or j = 2 or j = 3 or j = 4 by CQC_THE1:5; hence j = 1 or j = 2 or j = 3 or j = 4 by A1; end; Lm3: now let m be Nat; assume A1: m in Seg 5; then 1 <= m & m <= 5 by FINSEQ_1:3; then m = 0 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 by CQC_THE1:6; hence m = 1 or m = 2 or m = 3 or m = 4 or m = 5 by A1,FINSEQ_1:3; end; Lm4: now let A,L; let d be distance_function of A,L; succ {} c= DistEsti(d) or DistEsti(d) in succ {} by ORDINAL1:26; then succ {} c= DistEsti(d) or DistEsti(d) c= {} by ORDINAL1:34; then succ {} c= DistEsti(d) or DistEsti(d) = {} by XBOOLE_1:3; hence succ {} c= DistEsti(d) by Th23; end; theorem Th44: for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS being non empty set st FS = union { (S.i)`1 where i is Nat: not contradiction} holds union { (S.i)`2 where i is Nat: not contradiction} is distance_function of FS,L proof let S be ExtensionSeq of the carrier of L, BasicDF(L); let FS be non empty set; assume A1:FS = union { (S.i)`1 where i is Nat: not contradiction}; set FD = union { (S.i)`2 where i is Nat: not contradiction}; set A = the carrier of L; (S.0)`1 in { (S.i)`1 where i is Nat: not contradiction}; then reconsider X = { (S.i)`1 where i is Nat: not contradiction} as non empty set; reconsider FS as non empty set; A2: { (S.i)`2 where i is Nat: not contradiction} is c=-linear proof now let x,y be set; assume that A3: x in { (S.i)`2 where i is Nat: not contradiction} and A4: y in { (S.i)`2 where i is Nat: not contradiction}; consider k being Nat such that A5: x = (S.k)`2 by A3; consider l being Nat such that A6: y = (S.l)`2 by A4; k <= l or l <= k; then x c= y or y c= x by A5,A6,Th42; hence x,y are_c=-comparable by XBOOLE_0:def 9; end; hence thesis by ORDINAL1:def 9; end; { (S.i)`2 where i is Nat: not contradiction} c= PFuncs([:FS,FS:],A) proof let z be set; assume z in { (S.i)`2 where i is Nat: not contradiction}; then consider j being Nat such that A7: z = (S.j)`2; consider A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L such that Aq, dq is_extension_of A',d' and A8: S.j = [A',d'] & S.(j+1) = [Aq,dq] by Def21; A9: z = d' by A7,A8,MCART_1:def 2; A10: rng d' c= A; A11: dom d' = [:A',A':] by FUNCT_2:def 1; A' = (S.j)`1 by A8,MCART_1:def 1; then A' in { (S.i)`1 where i is Nat: not contradiction}; then A' c= FS by A1,ZFMISC_1:92; then dom d' c= [:FS,FS:] by A11,ZFMISC_1:119; hence z in PFuncs([:FS,FS:],A) by A9,A10,PARTFUN1:def 5; end; then FD in PFuncs([:FS,FS:],A) by A2,HAHNBAN:13; then consider g being Function such that A12: FD = g and dom g c= [:FS,FS:] and A13: rng g c= A by PARTFUN1:def 5; reconsider FD as Function by A12; A14: X is c=-linear proof now let x,y be set; assume that A15: x in X and A16: y in X; consider k being Nat such that A17: x = (S.k)`1 by A15; consider l being Nat such that A18: y = (S.l)`1 by A16; k <= l or l <= k; then x c= y or y c= x by A17,A18,Th41; hence x,y are_c=-comparable by XBOOLE_0:def 9; end; hence thesis by ORDINAL1:def 9; end; defpred X[set,set] means $2 = (S.$1)`2; A19: for x,y1,y2 being set st x in NAT & X[x,y1] & X[x,y2] holds y1 = y2; A20: for x being set st x in NAT ex y being set st X[x,y]; consider F being Function such that A21: dom F = NAT and A22: for x being set st x in NAT holds X[x,F.x] from FuncEx(A19,A20); A23: rng F = { (S.i)`2 where i is Nat: not contradiction} proof thus rng F c= { (S.i)`2 where i is Nat: not contradiction} proof let x be set; assume x in rng F; then consider j being set such that A24: j in dom F & F.j = x by FUNCT_1:def 5; reconsider j as Nat by A21,A24; x = (S.j)`2 by A22,A24; hence x in { (S.i)`2 where i is Nat: not contradiction}; end; let x be set; assume x in { (S.i)`2 where i is Nat: not contradiction}; then consider j being Nat such that A25: x = (S.j)`2; x = F.j by A22,A25; hence x in rng F by A21,FUNCT_1:def 5; end; F is Function-yielding proof let x be set; assume x in dom F; then reconsider j = x as Nat by A21; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A26: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21; (S.j)`2 = d1 by A26,MCART_1:def 2; hence F.x is Function by A22; end; then reconsider F as Function-yielding Function; set LL = { [:I,I:] where I is Element of X : I in X }, PP = { [:(S.i)`1,(S.i)`1:] where i is Nat: not contradiction }; A27: rng doms F = PP proof thus rng doms F c= PP proof let x be set; assume x in rng doms F; then consider j being set such that A28: j in dom doms F & x = (doms F).j by FUNCT_1:def 5; A29: j in dom F by A28,EXTENS_1:3; reconsider j as Nat by A21,A28,EXTENS_1:3; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A30: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21; A31: (S.j)`2 = d1 by A30,MCART_1:def 2; A32: (S.j)`1 = A1 by A30,MCART_1:def 1; x = dom (F.j) by A28,A29,FUNCT_6:31 .= dom d1 by A22,A31 .= [:(S.j)`1,(S.j)`1:] by A32,FUNCT_2:def 1; hence x in PP; end; let x be set; assume x in PP; then consider j being Nat such that A33:x = [:(S.j)`1,(S.j)`1:]; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A34: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21; A35: (S.j)`2 = d1 by A34,MCART_1:def 2; A36: (S.j)`1 = A1 by A34,MCART_1:def 1; j in NAT; then A37: j in dom doms F by A21,EXTENS_1:3; x = dom d1 by A33,A36,FUNCT_2:def 1 .= dom (F.j) by A22,A35 .= (doms F).j by A21,FUNCT_6:31; hence x in rng doms F by A37,FUNCT_1:def 5; end; LL = PP proof thus LL c= PP proof let x be set; assume x in LL; then consider J being Element of X such that A38:x = [:J,J:] and A39:J in X; consider j being Nat such that A40:J = (S.j)`1 by A39; thus x in PP by A38,A40; end; let x be set; assume x in PP; then consider j being Nat such that A41:x = [:(S.j)`1,(S.j)`1:]; (S.j)`1 in X; hence x in LL by A41; end; then [:FS,FS:] = union rng doms F by A1,A14,A27,Th3 .= dom FD by A23,Th1; then reconsider FD as BiFunction of FS,L by A12,A13,FUNCT_2:def 1,RELSET_1:11; A42: FD is zeroed proof let x be Element of FS; consider y being set such that A43: x in y & y in X by A1,TARSKI:def 4; consider j being Nat such that A44: y = (S.j)`1 by A43; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A45: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21; A46: (S.j)`2 = d1 by A45,MCART_1:def 2; reconsider x' = x as Element of A1 by A43,A44,A45,MCART_1:def 1; d1 in { (S.i)`2 where i is Nat: not contradiction} by A46; then A47: d1 c= FD by ZFMISC_1:92; A48: dom d1 = [:A1,A1:] by FUNCT_2:def 1; thus FD.(x,x) = FD.[x',x'] by BINOP_1:def 1 .= d1.[x',x'] by A47,A48,GRFUNC_1:8 .= d1.(x',x') by BINOP_1:def 1 .=Bottom L by Def7; end; A49: FD is symmetric proof let x,y be Element of FS; consider x1 being set such that A50: x in x1 & x1 in X by A1,TARSKI:def 4; consider k being Nat such that A51: x1 = (S.k)`1 by A50; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A52: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21; A53: (S.k)`2 = d1 by A52,MCART_1:def 2; A54: (S.k)`1 = A1 by A52,MCART_1:def 1; d1 in { (S.i)`2 where i is Nat: not contradiction} by A53; then A55: d1 c= FD by ZFMISC_1:92; A56: x in A1 by A50,A51,A52,MCART_1:def 1; consider y1 being set such that A57: y in y1 & y1 in X by A1,TARSKI:def 4; consider l being Nat such that A58: y1 = (S.l)`1 by A57; consider A2 being non empty set, d2 being distance_function of A2,L, Aq2 being non empty set, dq2 being distance_function of Aq2,L such that Aq2, dq2 is_extension_of A2,d2 and A59: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21; A60: (S.l)`2 = d2 by A59,MCART_1:def 2; A61: (S.l)`1 = A2 by A59,MCART_1:def 1; d2 in { (S.i)`2 where i is Nat: not contradiction} by A60; then A62: d2 c= FD by ZFMISC_1:92; A63: y in A2 by A57,A58,A59,MCART_1:def 1; per cases; suppose k <= l; then A1 c= A2 by A54,A61,Th41; then reconsider x'=x,y'=y as Element of A2 by A56,A57,A58,A59,MCART_1:def 1; A64: dom d2 = [:A2,A2:] by FUNCT_2:def 1; thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d2.[x',y'] by A62,A64,GRFUNC_1:8 .= d2.(x',y') by BINOP_1:def 1 .= d2.(y',x') by Def6 .= d2.[y',x'] by BINOP_1:def 1 .= FD.[y',x'] by A62,A64,GRFUNC_1:8 .= FD.(y,x) by BINOP_1:def 1; suppose l <= k; then A2 c= A1 by A54,A61,Th41; then reconsider x'=x,y'=y as Element of A1 by A50,A51,A52,A63,MCART_1:def 1; A65: dom d1 = [:A1,A1:] by FUNCT_2:def 1; thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d1.[x',y'] by A55,A65,GRFUNC_1:8 .= d1.(x',y') by BINOP_1:def 1 .= d1.(y',x') by Def6 .= d1.[y',x'] by BINOP_1:def 1 .= FD.[y',x'] by A55,A65,GRFUNC_1:8 .= FD.(y,x) by BINOP_1:def 1; end; FD is u.t.i. proof let x,y,z be Element of FS; consider x1 being set such that A66: x in x1 & x1 in X by A1,TARSKI:def 4; consider k being Nat such that A67: x1 = (S.k)`1 by A66; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that Aq1, dq1 is_extension_of A1,d1 and A68: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21; A69: (S.k)`2 = d1 by A68,MCART_1:def 2; A70: (S.k)`1 = A1 by A68,MCART_1:def 1; d1 in { (S.i)`2 where i is Nat: not contradiction} by A69; then A71: d1 c= FD by ZFMISC_1:92; A72: x in A1 by A66,A67,A68,MCART_1:def 1; A73: dom d1 = [:A1,A1:] by FUNCT_2:def 1; consider y1 being set such that A74: y in y1 & y1 in X by A1,TARSKI:def 4; consider l being Nat such that A75: y1 = (S.l)`1 by A74; consider A2 being non empty set, d2 being distance_function of A2,L, Aq2 being non empty set, dq2 being distance_function of Aq2,L such that Aq2, dq2 is_extension_of A2,d2 and A76: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21; A77: (S.l)`2 = d2 by A76,MCART_1:def 2; A78: (S.l)`1 = A2 by A76,MCART_1:def 1; d2 in { (S.i)`2 where i is Nat: not contradiction} by A77; then A79: d2 c= FD by ZFMISC_1:92; A80: y in A2 by A74,A75,A76,MCART_1:def 1; A81: dom d2 = [:A2,A2:] by FUNCT_2:def 1; consider z1 being set such that A82: z in z1 & z1 in X by A1,TARSKI:def 4; consider n being Nat such that A83: z1 = (S.n)`1 by A82; consider A3 being non empty set, d3 being distance_function of A3,L, Aq3 being non empty set, dq3 being distance_function of Aq3,L such that Aq3, dq3 is_extension_of A3,d3 and A84: S.n = [A3,d3] & S.(n+1) = [Aq3,dq3] by Def21; A85: (S.n)`2 = d3 by A84,MCART_1:def 2; A86: (S.n)`1 = A3 by A84,MCART_1:def 1; d3 in { (S.i)`2 where i is Nat: not contradiction} by A85; then A87: d3 c= FD by ZFMISC_1:92; A88: z in A3 by A82,A83,A84,MCART_1:def 1; A89: dom d3 = [:A3,A3:] by FUNCT_2:def 1; per cases; suppose k <= l; then A90: A1 c= A2 by A70,A78,Th41; thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) proof per cases; suppose l <= n; then A91: A2 c= A3 by A78,A86,Th41; then A1 c= A3 by A90,XBOOLE_1:1; then reconsider x' = x, y' = y, z' = z as Element of A3 by A72,A80,A82,A83,A84,A91,MCART_1:def 1; A92: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d3.[x',y'] by A87,A89,GRFUNC_1:8 .= d3.(x',y') by BINOP_1:def 1; A93: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1 .= d3.[y',z'] by A87,A89,GRFUNC_1:8 .= d3.(y',z') by BINOP_1:def 1; FD.(x,z) = FD.[x',z'] by BINOP_1:def 1 .= d3.[x',z'] by A87,A89,GRFUNC_1:8 .= d3.(x',z') by BINOP_1:def 1; hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A92,A93,Def8; suppose n <= l; then A3 c= A2 by A78,A86,Th41; then reconsider x' = x, y' = y, z' = z as Element of A2 by A72,A74,A75,A76,A88,A90,MCART_1:def 1; A94: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d2.[x',y'] by A79,A81,GRFUNC_1:8 .= d2.(x',y') by BINOP_1:def 1; A95: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1 .= d2.[y',z'] by A79,A81,GRFUNC_1:8 .= d2.(y',z') by BINOP_1:def 1; FD.(x,z) = FD.[x',z'] by BINOP_1:def 1 .= d2.[x',z'] by A79,A81,GRFUNC_1:8 .= d2.(x',z') by BINOP_1:def 1; hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A94,A95,Def8; end; suppose l <= k; then A96: A2 c= A1 by A70,A78,Th41; thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) proof per cases; suppose k <= n; then A97: A1 c= A3 by A70,A86,Th41; then A2 c= A3 by A96,XBOOLE_1:1; then reconsider x' = x, y' = y, z' = z as Element of A3 by A72,A80,A82,A83,A84,A97,MCART_1:def 1; A98: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d3.[x',y'] by A87,A89,GRFUNC_1:8 .= d3.(x',y') by BINOP_1:def 1; A99: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1 .= d3.[y',z'] by A87,A89,GRFUNC_1:8 .= d3.(y',z') by BINOP_1:def 1; FD.(x,z) = FD.[x',z'] by BINOP_1:def 1 .= d3.[x',z'] by A87,A89,GRFUNC_1:8 .= d3.(x',z') by BINOP_1:def 1; hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A98,A99,Def8; suppose n <= k; then A3 c= A1 by A70,A86,Th41; then reconsider x' = x, y' = y, z' = z as Element of A1 by A66,A67,A68,A80,A88,A96,MCART_1:def 1; A100: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d1.[x',y'] by A71,A73,GRFUNC_1:8 .= d1.(x',y') by BINOP_1:def 1; A101: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1 .= d1.[y',z'] by A71,A73,GRFUNC_1:8 .= d1.(y',z') by BINOP_1:def 1; FD.(x,z) = FD.[x',z'] by BINOP_1:def 1 .= d1.[x',z'] by A71,A73,GRFUNC_1:8 .= d1.(x',z') by BINOP_1:def 1; hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A100,A101,Def8; end; end; hence thesis by A42,A49; end; theorem Th45: for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS being non empty set, FD being distance_function of FS,L for x,y being Element of FS for a,b being Element of L st FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} & FD.(x,y) <= a"\/"b ex z1,z2,z3 being Element of FS st FD.(x,z1) = a & FD.(z2,z3) = a & FD.(z1,z2) = b & FD.(z3,y) = b proof let S be ExtensionSeq of the carrier of L, BasicDF(L); let FS be non empty set, FD be distance_function of FS,L; let x,y be Element of FS; let a,b be Element of L; assume that A1: FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} and A2: FD.(x,y) <= a"\/"b; (S.0)`1 in { (S.i)`1 where i is Nat: not contradiction}; then reconsider X = { (S.i)`1 where i is Nat: not contradiction} as non empty set; consider x1 being set such that A3: x in x1 & x1 in X by A1,TARSKI:def 4; consider k being Nat such that A4: x1 = (S.k)`1 by A3; consider A1 being non empty set, d1 being distance_function of A1,L, Aq1 being non empty set, dq1 being distance_function of Aq1,L such that A5: Aq1, dq1 is_extension_of A1,d1 and A6: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21; A7: (S.k)`2 = d1 by A6,MCART_1:def 2; A8: (S.k)`1 = A1 by A6,MCART_1:def 1; A9: (S.(k+1))`1 = Aq1 by A6,MCART_1:def 1; A10: (S.(k+1))`2 = dq1 by A6,MCART_1:def 2; d1 in { (S.i)`2 where i is Nat: not contradiction} by A7; then A11: d1 c= FD by A1,ZFMISC_1:92; dq1 in { (S.i)`2 where i is Nat: not contradiction} by A10; then A12: dq1 c= FD by A1,ZFMISC_1:92; Aq1 in { (S.i)`1 where i is Nat: not contradiction} by A9; then A13: Aq1 c= FS by A1,ZFMISC_1:92; A14: x in A1 by A3,A4,A6,MCART_1:def 1; consider y1 being set such that A15: y in y1 & y1 in X by A1,TARSKI:def 4; consider l being Nat such that A16: y1 = (S.l)`1 by A15; consider A2 being non empty set, d2 being distance_function of A2,L, Aq2 being non empty set, dq2 being distance_function of Aq2,L such that A17: Aq2, dq2 is_extension_of A2,d2 and A18: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21; A19: (S.l)`2 = d2 by A18,MCART_1:def 2; A20: (S.l)`1 = A2 by A18,MCART_1:def 1; A21: (S.(l+1))`1 = Aq2 by A18,MCART_1:def 1; A22: (S.(l+1))`2 = dq2 by A18,MCART_1:def 2; d2 in { (S.i)`2 where i is Nat: not contradiction} by A19; then A23: d2 c= FD by A1,ZFMISC_1:92; dq2 in { (S.i)`2 where i is Nat: not contradiction} by A22; then A24: dq2 c= FD by A1,ZFMISC_1:92; Aq2 in { (S.i)`1 where i is Nat: not contradiction} by A21; then A25: Aq2 c= FS by A1,ZFMISC_1:92; A26: y in A2 by A15,A16,A18,MCART_1:def 1; per cases; suppose k <= l; then A1 c= A2 by A8,A20,Th41; then reconsider x'=x,y'=y as Element of A2 by A14,A15,A16,A18,MCART_1:def 1; A27: x' in A2 & y' in A2; A28: dom d2 = [:A2,A2:] by FUNCT_2:def 1; FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d2.[x',y'] by A23,A28,GRFUNC_1:8 .= d2.(x',y') by BINOP_1:def 1; then consider z1,z2,z3 being Element of Aq2 such that A29: dq2.(x,z1) = a and A30: dq2.(z2,z3) = a and A31: dq2.(z1,z2) = b and A32: dq2.(z3,y) = b by A2,A17,Th40; z1 in Aq2 & z2 in Aq2 & z3 in Aq2; then reconsider z1' = z1, z2' = z2, z3' = z3 as Element of FS by A25; l <= l+1 by NAT_1:29; then A2 c= Aq2 by A20,A21,Th41; then reconsider x'' = x',y'' = y' as Element of Aq2 by A27; A33: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1; take z1',z2',z3'; thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1 .= dq2.[x'',z1] by A24,A33,GRFUNC_1:8 .= a by A29,BINOP_1:def 1; thus FD.(z2',z3') = FD.[z2,z3] by BINOP_1:def 1 .= dq2.[z2,z3] by A24,A33,GRFUNC_1:8 .= a by A30,BINOP_1:def 1; thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1 .= dq2.[z1,z2] by A24,A33,GRFUNC_1:8 .= b by A31,BINOP_1:def 1; thus FD.(z3',y) = FD.[z3,y''] by BINOP_1:def 1 .= dq2.[z3,y''] by A24,A33,GRFUNC_1:8 .= b by A32,BINOP_1:def 1; suppose l <= k; then A2 c= A1 by A8,A20,Th41; then reconsider x'=x,y'=y as Element of A1 by A3,A4,A6,A26,MCART_1:def 1; A34: x' in A1 & y' in A1; A35: dom d1 = [:A1,A1:] by FUNCT_2:def 1; FD.(x,y) = FD.[x',y'] by BINOP_1:def 1 .= d1.[x',y'] by A11,A35,GRFUNC_1:8 .= d1.(x',y') by BINOP_1:def 1; then consider z1,z2,z3 being Element of Aq1 such that A36: dq1.(x,z1) = a and A37: dq1.(z2,z3) = a and A38: dq1.(z1,z2) = b and A39: dq1.(z3,y) = b by A2,A5,Th40; z1 in Aq1 & z2 in Aq1 & z3 in Aq1; then reconsider z1' = z1, z2' = z2, z3' = z3 as Element of FS by A13; k <= k+1 by NAT_1:29; then A1 c= Aq1 by A8,A9,Th41; then reconsider x'' = x',y'' = y' as Element of Aq1 by A34; A40: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1; take z1',z2',z3'; thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1 .= dq1.[x'',z1] by A12,A40,GRFUNC_1:8 .= a by A36,BINOP_1:def 1; thus FD.(z2',z3') = FD.[z2,z3] by BINOP_1:def 1 .= dq1.[z2,z3] by A12,A40,GRFUNC_1:8 .= a by A37,BINOP_1:def 1; thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1 .= dq1.[z1,z2] by A12,A40,GRFUNC_1:8 .= b by A38,BINOP_1:def 1; thus FD.(z3',y) = FD.[z3,y''] by BINOP_1:def 1 .= dq1.[z3,y''] by A12,A40,GRFUNC_1:8 .= b by A39,BINOP_1:def 1; end; theorem Th46: for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS being non empty set for FD being distance_function of FS,L for f being Homomorphism of L,EqRelLATT FS for x, y being Element of FS for e1,e2 being Equivalence_Relation of FS,x,y st f = alpha FD & FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} & e1 in the carrier of Image f & e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty FinSequence of FS st len F = 3+2 & x,y are_joint_by F,e1,e2 proof let S be ExtensionSeq of the carrier of L, BasicDF(L); let FS be non empty set; let FD be distance_function of FS,L; let f be Homomorphism of L,EqRelLATT FS; let x, y be Element of FS; let e1,e2 be Equivalence_Relation of FS,x,y; assume that A1: f = alpha FD and A2: FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} and A3: e1 in the carrier of Image f & e2 in the carrier of Image f and A4: [x,y] in e1 "\/" e2; Image f = subrelstr rng f by YELLOW_2:def 2; then A5:the carrier of Image f = rng f by YELLOW_0:def 15; then consider a being set such that A6: a in dom f and A7: e1 = f.a by A3,FUNCT_1:def 5; consider b being set such that A8: b in dom f and A9: e2 = f.b by A3,A5,FUNCT_1:def 5; reconsider a,b as Element of L by A6,A8; field (e1 "\/" e2) = FS by EQREL_1:15; then reconsider u = x, v = y as Element of FS by A4,RELAT_1:30; reconsider a,b as Element of L; consider e1' being Equivalence_Relation of FS such that A10: e1' = f.a and A11: for u,v being Element of FS holds [u,v] in e1' iff FD.(u,v) <= a by A1,Def9; consider e2' being Equivalence_Relation of FS such that A12: e2' = f.b and A13: for u,v being Element of FS holds [u,v] in e2' iff FD.(u,v) <= b by A1,Def9; consider e being Equivalence_Relation of FS such that A14: e = f.(a"\/"b) and A15: for u,v being Element of FS holds [u,v] in e iff FD.(u,v) <= a"\/"b by A1,Def9; e = f.a"\/"f.b by A14,WAYBEL_6:2 .= e1 "\/" e2 by A7,A9,Th10; then FD.(u,v) <= a"\/"b by A4,A15; then consider z1,z2,z3 being Element of FS such that A16: FD.(u,z1) = a and A17: FD.(z2,z3) = a and A18: FD.(z1,z2) = b and A19: FD.(z3,v) = b by A2,Th45; defpred P[set,set] means ($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2 = v); A20: for m being Nat, w1,w2 being set st m in Seg 5 & P[m,w1] & P[m,w2] holds w1 = w2 by Lm3; A21: for m being Nat st m in Seg 5 ex w being set st P[m,w] proof let m be Nat; assume A22:m in Seg 5; per cases by A22,Lm3; suppose A23: m = 1; take w = x; thus P[m,w] by A23; suppose A24: m = 2; take w = z1; thus P[m,w] by A24; suppose A25: m = 3; take w = z2; thus P[m,w] by A25; suppose A26: m = 4; take w = z3; thus P[m,w] by A26; suppose A27: m = 5; take w = y; thus P[m,w] by A27; end; ex p being FinSequence st dom p = Seg 5 & for k being Nat st k in Seg 5 holds P[k,p.k] from SeqEx(A20,A21); then consider h being FinSequence such that A28: dom h = Seg 5 and A29: for m being Nat st m in Seg 5 holds (m = 1 implies h.m = u) & (m = 2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) & (m = 5 implies h.m = v); Seg 5 = { n where n is Nat: 1 <= n & n <= 5 } by FINSEQ_1:def 1; then A30: 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5; A31: len h = 5 by A28,FINSEQ_1:def 3; rng h c= FS proof let w be set; assume w in rng h; then consider j be set such that A32: j in dom h & w = h.j by FUNCT_1:def 5; per cases by A28,A32,Lm3; suppose j = 1; then h.j = u by A29,A30; hence w in FS by A32; suppose j = 2; then h.j = z1 by A29,A30; hence w in FS by A32; suppose j = 3; then h.j = z2 by A29,A30; hence w in FS by A32; suppose j = 4; then h.j = z3 by A29,A30; hence w in FS by A32; suppose j = 5; then h.j = v by A29,A30; hence w in FS by A32; end; then reconsider h as FinSequence of FS by FINSEQ_1:def 4; len h <> 0 by A28,FINSEQ_1:def 3; then reconsider h as non empty FinSequence of FS by FINSEQ_1:25; take h; thus len h = 3+2 by A28,FINSEQ_1:def 3; A33: h.1 = x by A29,A30; A34: h.(len h) = h.5 by A28,FINSEQ_1:def 3 .= y by A29,A30; for j being Nat st 1 <= j & j < len h holds (j is odd implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2) proof let j be Nat; assume A35: 1 <= j & j < len h; per cases by A31,A35,Lm2; suppose j = 1; then A36: 2*0+1 = j; [u,z1] in e1' by A11,A16; then [h.1,z1] in e1' by A29,A30; hence (j is odd implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2) by A7,A10,A29,A30,A36; suppose j = 3; then A37: 2*1+1 = j; [z2,z3] in e1' by A11,A17; then [h.3,z3] in e1' by A29,A30; hence (j is odd implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2) by A7,A10,A29,A30,A37; suppose j = 2; then A38: 2*1 = j; [z1,z2] in e2' by A13,A18; then [h.2,z2] in e2' by A29,A30; hence (j is odd implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2) by A9,A12,A29,A30,A38; suppose j = 4; then A39: 2*2 = j; [z3,v] in e2' by A13,A19; then [h.4,v] in e2' by A29,A30; hence (j is odd implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2) by A9,A12,A29,A30,A39; end; hence x,y are_joint_by h,e1,e2 by A33,A34,Def3; end; theorem ex A being non empty set, f being Homomorphism of L,EqRelLATT A st f is one-to-one & type_of Image f <= 3 proof set A = the carrier of L, D = BasicDF(L); A1: D is onto by Th43; consider S being ExtensionSeq of A,D; set FS = union { (S.i)`1 where i is Nat: not contradiction}; A2: S.0 = [A,D] by Def21; then A3: (S.0)`1 = A by MCART_1:def 1; (S.0)`1 in { (S.i)`1 where i is Nat: not contradiction}; then A4: A c= FS by A3,ZFMISC_1:92; consider xx being set such that A5: xx in A by XBOOLE_0:def 1; reconsider FS as non empty set by A4,A5; reconsider FD = union { (S.i)`2 where i is Nat: not contradiction} as distance_function of FS,L by Th44; A6: FD is onto proof A7: rng D = A by A1,FUNCT_2:def 3; for w being set st w in A ex z being set st z in [:FS,FS:] & w = FD.z proof let w be set; assume w in A; then consider z being set such that A8: z in [:A,A:] and A9: D.z = w by A7,FUNCT_2:17; take z; A10: S.0 = [A,D] by Def21; then A11: A = (S.0)`1 by MCART_1:def 1; (S.0)`1 in { (S.i)`1 where i is Nat: not contradiction}; then A c= FS by A11,ZFMISC_1:92; then [:A,A:] c= [:FS,FS:] by ZFMISC_1:119; hence z in [:FS,FS:] by A8; A12: z in dom D by A8,FUNCT_2:def 1; A13: D = (S.0)`2 by A10,MCART_1:def 2; (S.0)`2 in { (S.i)`2 where i is Nat: not contradiction}; then D c= FD by A13,ZFMISC_1:92; hence w = FD.z by A9,A12,GRFUNC_1:8; end; then rng FD = A by FUNCT_2:16; hence FD is onto by FUNCT_2:def 3; end; alpha FD is join-preserving proof let a,b be Element of L; set f = alpha FD; A14:ex_sup_of f.:{a,b},EqRelLATT FS by YELLOW_0:17; A15: dom f = the carrier of L by FUNCT_2:def 1; consider e1 being Equivalence_Relation of FS such that A16: e1 = f.a and A17: for x,y being Element of FS holds [x,y] in e1 iff FD.(x,y) <= a by Def9; consider e2 being Equivalence_Relation of FS such that A18: e2 = f.b and A19: for x,y being Element of FS holds [x,y] in e2 iff FD.(x,y) <= b by Def9; consider e3 being Equivalence_Relation of FS such that A20: e3 = f.(a "\/" b) and A21: for x,y being Element of FS holds [x,y] in e3 iff FD.(x,y) <= a"\/"b by Def9; A22: field e1 = FS by EQREL_1:15; A23: field e2 = FS by EQREL_1:15; A24: field e3 = FS by EQREL_1:15; A25: e1 "\/" e2 c= e3 proof now let x,y be set; assume A26:[x,y] in e1; then reconsider x' = x, y' = y as Element of FS by A22,RELAT_1:30; A27:FD.(x',y') <= a by A17,A26; a <= a "\/" b by YELLOW_0:22; then FD.(x',y') <= a "\/" b by A27,ORDERS_1:26; hence [x,y] in e3 by A21; end; then A28: e1 c= e3 by RELAT_1:def 3; now let x,y be set; assume A29:[x,y] in e2; then reconsider x' = x, y' = y as Element of FS by A23,RELAT_1:30; A30:FD.(x',y') <= b by A19,A29; b <= b "\/" a by YELLOW_0:22; then FD.(x',y') <= b "\/" a by A30,ORDERS_1:26; hence [x,y] in e3 by A21; end; then e2 c= e3 by RELAT_1:def 3; then e1 \/ e2 c= e3 by A28,XBOOLE_1:8; hence thesis by EQREL_1:def 3; end; A31: e3 c= e1 "\/" e2 proof for u,v being set holds [u,v] in e3 implies [u,v] in e1 "\/" e2 proof let u,v be set; assume A32: [u,v] in e3; then reconsider x = u, y = v as Element of FS by A24,RELAT_1:30; A33: u in FS by A24,A32,RELAT_1:30; FD.(x,y) <= a"\/"b by A21,A32; then consider z1,z2,z3 being Element of FS such that A34: FD.(x,z1) = a and A35: FD.(z2,z3) = a and A36: FD.(z1,z2) = b and A37: FD.(z3,y) = b by Th45; defpred P[set,set] means ($1 = 1 implies $2 = x) & ($1 = 2 implies $2 = z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2 = y); A38: for m being Nat, w1,w2 being set st m in Seg 5 & P[m,w1] & P[m,w2] holds w1 = w2 by Lm3; A39: for m being Nat st m in Seg 5 ex w being set st P[m,w] proof let m be Nat; assume A40:m in Seg 5; per cases by A40,Lm3; suppose A41: m = 1; take w = x; thus P[m,w] by A41; suppose A42: m = 2; take w = z1; thus P[m,w] by A42; suppose A43: m = 3; take w = z2; thus P[m,w] by A43; suppose A44: m = 4; take w = z3; thus P[m,w] by A44; suppose A45: m = 5; take w = y; thus P[m,w] by A45; end; ex p being FinSequence st dom p = Seg 5 & for k being Nat st k in Seg 5 holds P[k,p.k] from SeqEx(A38,A39); then consider h being FinSequence such that A46: dom h = Seg 5 and A47: for m being Nat st m in Seg 5 holds (m = 1 implies h.m = x) & (m = 2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) & (m = 5 implies h.m = y); Seg 5 = { n where n is Nat: 1 <= n & n <= 5 } by FINSEQ_1:def 1; then A48: 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5; A49: len h = 5 by A46,FINSEQ_1:def 3; A50: u = h.1 by A47,A48; A51: v = h.5 by A47,A48 .= h.(len h) by A46,FINSEQ_1:def 3; for j being Nat st 1 <= j & j < len h holds [h.j,h.(j+1)] in e1 \/ e2 proof let j be Nat; assume A52: 1 <= j & j < len h; per cases by A49,A52,Lm2; suppose A53:j = 1; [x,z1] in e1 by A17,A34; then [h.1,z1] in e1 by A47,A48; then [h.1,h.2] in e1 by A47,A48; hence [h.j,h.(j+1)] in e1 \/ e2 by A53,XBOOLE_0:def 2; suppose A54:j = 3; [z2,z3] in e1 by A17,A35; then [h.3,z3] in e1 by A47,A48; then [h.3,h.4] in e1 by A47,A48; hence [h.j,h.(j+1)] in e1 \/ e2 by A54,XBOOLE_0:def 2; suppose A55:j = 2; [z1,z2] in e2 by A19,A36; then [h.2,z2] in e2 by A47,A48; then [h.2,h.3] in e2 by A47,A48; hence [h.j,h.(j+1)] in e1 \/ e2 by A55,XBOOLE_0:def 2; suppose A56:j = 4; [z3,y] in e2 by A19,A37; then [h.4,y] in e2 by A47,A48; then [h.4,h.5] in e2 by A47,A48; hence [h.j,h.(j+1)] in e1 \/ e2 by A56,XBOOLE_0:def 2; end; hence [u,v] in e1 "\/" e2 by A33,A49,A50,A51,EQREL_1:36; end; hence thesis by RELAT_1:def 3; end; sup (f.:{a,b}) = sup {f.a,f.b} by A15,FUNCT_1:118 .= f.a "\/" f.b by YELLOW_0:41 .= e1 "\/" e2 by A16,A18,Th10 .= f.(a "\/" b) by A20,A25,A31,XBOOLE_0:def 10 .= f.sup {a,b} by YELLOW_0:41; hence f preserves_sup_of {a,b} by A14,WAYBEL_0:def 31; end; then reconsider f = alpha FD as Homomorphism of L,EqRelLATT FS by Th16; take FS,f; thus f is one-to-one by A6,Th17; A57: Image f = subrelstr rng f by YELLOW_2:def 2; A58:dom f = the carrier of L by FUNCT_2:def 1; A59: ex e being Equivalence_Relation of FS st e in the carrier of Image f & e <> id FS proof consider A' being non empty set, d' being distance_function of A',L, Aq' being non empty set, dq' being distance_function of Aq',L such that A60: Aq', dq' is_extension_of A',d' and A61: S.0 = [A',d'] & S.(0+1) = [Aq',dq'] by Def21; A' = A & d' = D by A2,A61,ZFMISC_1:33; then consider q being QuadrSeq of D such that A62: Aq' = NextSet(D) and A63: dq' = NextDelta(q) by A60,Def20; A64: (S.1)`2 = NextDelta(q) by A61,A63,MCART_1:def 2; (S.1)`2 in { (S.i)`2 where i is Nat: not contradiction}; then A65: NextDelta(q) c= FD by A64,ZFMISC_1:92; A66: (S.1)`1 = NextSet(D) by A61,A62,MCART_1:def 1; (S.1)`1 in { (S.i)`1 where i is Nat: not contradiction}; then A67: NextSet(D) c= FS by A66,ZFMISC_1:92; succ {} c= DistEsti(D) by Lm4; then {} in DistEsti(D) by ORDINAL1:33; then A68: {} in dom q by Th28; then q.{} in rng q by FUNCT_1:def 5; then q.{} in {[u,v,a',b'] where u is Element of A, v is Element of A, a' is Element of L, b' is Element of L: D.(u,v) <= a'"\/"b'} by Def14; then consider u,v be Element of A, a,b be Element of L such that A69: q.{} = [u,v,a,b] & D.(u,v) <= a"\/"b; ConsecutiveSet(A,{}) = A by Th24; then reconsider Q = Quadr(q,{}) as Element of [:A,A,the carrier of L,the carrier of L:]; A70: Quadr(q,{}) = [u,v,a,b] by A68,A69,Def15; consider e being Equivalence_Relation of FS such that A71: e = f.b and A72: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b by Def9; take e; e in rng f by A58,A71,FUNCT_1:def 5; hence e in the carrier of Image f by A57,YELLOW_0:def 15; A73: new_set A = new_set ConsecutiveSet(A,{}) by Th24 .= ConsecutiveSet(A,succ {}) by Th25; A74: NextSet(D) = ConsecutiveSet(A,DistEsti(D)) by Def18; A75: succ {} c= DistEsti(D) by Lm4; then A76: new_set A c= NextSet(D) by A73,A74,Th32; A77: ConsecutiveSet(A,{}) = A & ConsecutiveDelta(q,{}) = D by Th24,Th29; A78: ConsecutiveDelta(q,succ {}) = new_bi_fun(BiFun(ConsecutiveDelta(q,{}), ConsecutiveSet(A,{}),L),Quadr(q,{})) by Th30 .= new_bi_fun(D,Q) by A77,Def16; ConsecutiveDelta(q,DistEsti(D)) = NextDelta(q) by Def19; then new_bi_fun(D,Q) c= NextDelta(q) by A75,A78,Th35; then A79: new_bi_fun(D,Q) c= FD by A65,XBOOLE_1:1; A80: new_set A c= FS by A67,A76,XBOOLE_1:1; A81: dom new_bi_fun(D,Q) = [:new_set A,new_set A:] by FUNCT_2:def 1; {A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14; then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; then A82: {A} in new_set A by Def10; {{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14; then {{A}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2; then A83: {{A}} in new_set A by Def10; then A84: [{A},{{A}}] in dom new_bi_fun(D,Q) by A81,A82,ZFMISC_1:106; reconsider W = {A}, V = {{A}} as Element of FS by A80,A82,A83; FD.(W,V) = FD.[{A},{{A}}] by BINOP_1:def 1 .= new_bi_fun(D,Q).[{A},{{A}}] by A79,A84,GRFUNC_1:8 .= new_bi_fun(D,Q).({A},{{A}}) by BINOP_1:def 1 .= Q`4 by Def11 .= b by A70,MCART_1:def 11; then A85: [{A},{{A}}] in e by A72; {A} <> {{A}} proof assume {A} = {{A}}; then {A} in {A} by TARSKI:def 1; hence contradiction; end; hence e <> id FS by A85,RELAT_1:def 10; end; for e1,e2 being Equivalence_Relation of FS,x,y st e1 in the carrier of Image f & e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty FinSequence of FS st len F = 3+2 & x,y are_joint_by F,e1,e2 by Th46; hence type_of Image f <= 3 by A59,Th15; end;

Back to top