:: More on the Lattice of Many Sorted Equivalence Relations :: by Robert Milewski :: :: Received February 9, 1996 :: Copyright (c) 1996-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, PBOOLE, REAL_1, STRUCT_0, MSUALG_5, EQREL_1, RELAT_1, FUNCT_1, MSUALG_4, TARSKI, ZFMISC_1, XXREAL_2, SUBSET_1, LATTICES, CLOSURE2, SETFAM_1, FUNCT_4, REWRITE1, LATTICE3, MSSUBFAM, NAT_LAT, REALSET1, XXREAL_0, XXREAL_1, REAL_LAT, BINOP_1, SUPINF_1, ORDINAL2, ARYTM_1, CARD_1, ARYTM_3, MSUALG_7, SETLIM_2, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SUPINF_1, ORDINAL1, FUNCT_7, XXREAL_0, REAL_1, XXREAL_2, XCMPLX_0, XREAL_0, STRUCT_0, RELSET_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, NUMBERS, RCOMP_1, EQREL_1, BINOP_1, REALSET1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, MSUALG_3, MSUALG_4, MSUALG_5, SETFAM_1, MSSUBFAM, CLOSURE2; constructors BINOP_1, REAL_1, SQUARE_1, SUPINF_1, RCOMP_1, REALSET1, MSSUBFAM, REAL_LAT, LATTICE3, MSUALG_3, MSUALG_5, CLOSURE2, XXREAL_2, RELSET_1, FUNCT_7; registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, LATTICE3, XXREAL_2; equalities BINOP_1, REALSET1; expansions TARSKI, LATTICE3, XXREAL_2; theorems TARSKI, PBOOLE, MSSUBFAM, LATTICE3, VECTSP_8, MSUALG_4, MSUALG_5, ZFMISC_1, SETFAM_1, EQREL_1, LATTICES, NAT_LAT, FUNCT_1, REAL_LAT, FUNCT_2, RCOMP_1, MSUALG_3, CLOSURE2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NUMBERS, RELAT_1, XXREAL_2, XREAL_0; schemes DOMAIN_1; begin :: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS IS COMPLETE reserve I for non empty set; reserve M for ManySortedSet of I; reserve Y,x,y,i for set; reserve r,r1,r2 for Real; theorem Th1: id M is Equivalence_Relation of M proof set J = id M; for i be set st i in I holds J.i is Relation of M.i proof let i be set; assume i in I; then J.i = id (M.i) by MSUALG_3:def 1; hence thesis; end; then reconsider J as ManySortedRelation of M by MSUALG_4:def 1; for i be set, R be Relation of M.i st i in I & J.i = R holds R is Equivalence_Relation of M.i proof let i be set; let R be Relation of M.i; assume that A1: i in I and A2: J.i = R; J.i = id (M.i) by A1,MSUALG_3:def 1; hence thesis by A2,EQREL_1:3; end; hence thesis by MSUALG_4:def 2; end; theorem Th2: [|M,M|] is Equivalence_Relation of M proof set J = [|M,M|]; for i be set st i in I holds J.i is Relation of M.i proof let i be set; assume i in I; then J.i c= [:M.i,M.i:] by PBOOLE:def 16; hence thesis; end; then reconsider J as ManySortedRelation of M by MSUALG_4:def 1; for i be set, R be Relation of M.i st i in I & J.i = R holds R is Equivalence_Relation of M.i proof let i be set; let R be Relation of M.i; assume that A1: i in I and A2: J.i = R; J.i = [:M.i,M.i:] by A1,PBOOLE:def 16 .= nabla M.i by EQREL_1:def 1; hence thesis by A2,EQREL_1:4; end; hence thesis by MSUALG_4:def 2; end; registration let I,M; cluster EqRelLatt M -> bounded; coherence proof ex c being Element of EqRelLatt M st for a being Element of EqRelLatt M holds c"\/"a = c & a"\/"c = c proof reconsider c9 = [|M,M|] as Equivalence_Relation of M by Th2; reconsider c = c9 as Element of EqRelLatt M by MSUALG_5:def 5; take c; let a be Element of EqRelLatt M; reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5; A1: now let i be object; A2: ex K1 be ManySortedRelation of M st K1 = c9 (\/) a9 & c9 "\/" a9 = EqCl K1 by MSUALG_5:def 4; assume A3: i in I; then reconsider i9 = i as Element of I; reconsider K2 = c9.i9, a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2; (c9 (\/) a9).i = c9.i \/ a9.i by A3,PBOOLE:def 4 .= [:M.i,M.i:] \/ a9.i by A3,PBOOLE:def 16 .= nabla M.i \/ a2 by EQREL_1:def 1 .= nabla M.i by EQREL_1:1 .= [:M.i,M.i:] by EQREL_1:def 1 .= c9.i by A3,PBOOLE:def 16; hence (c9 "\/" a9).i = EqCl K2 by A2,MSUALG_5:def 3 .= c9.i by MSUALG_5:2; end; thus c"\/"a = (the L_join of EqRelLatt M).(c,a) by LATTICES:def 1 .= c9 "\/" a9 by MSUALG_5:def 5 .= c by A1,PBOOLE:3; hence thesis; end; then A4: EqRelLatt M is upper-bounded by LATTICES:def 14; ex c being Element of EqRelLatt M st for a being Element of EqRelLatt M holds c"/\"a = c & a"/\"c = c proof reconsider c9 = id M as Equivalence_Relation of M by Th1; reconsider c = c9 as Element of EqRelLatt M by MSUALG_5:def 5; take c; let a be Element of EqRelLatt M; reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5; A5: now let i be object; assume A6: i in I; then reconsider i9 = i as Element of I; reconsider a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2; thus (c9 (/\) a9).i = c9.i /\ a9.i by A6,PBOOLE:def 5 .= id (M.i) /\ a2 by MSUALG_3:def 1 .= id (M.i) by EQREL_1:10 .= c9.i by A6,MSUALG_3:def 1; end; thus c"/\"a = (the L_meet of EqRelLatt M).(c,a) by LATTICES:def 2 .= c9 (/\) a9 by MSUALG_5:def 5 .= c by A5,PBOOLE:3; hence thesis; end; then EqRelLatt M is lower-bounded by LATTICES:def 13; hence thesis by A4; end; end; theorem Bottom EqRelLatt M = id M proof set K = id M; K is Equivalence_Relation of M by Th1; then reconsider K as Element of EqRelLatt M by MSUALG_5:def 5; now let a be Element of EqRelLatt M; reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5; A1: now let i be object; assume A2: i in I; then reconsider i9 = i as Element of I; reconsider a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2; thus (K9 (/\) a9).i = K9.i /\ a9.i by A2,PBOOLE:def 5 .= id (M.i) /\ a2 by MSUALG_3:def 1 .= id (M.i) by EQREL_1:10 .= K9.i by A2,MSUALG_3:def 1; end; thus K "/\" a = (the L_meet of EqRelLatt M).(K,a) by LATTICES:def 2 .= K9 (/\) a9 by MSUALG_5:def 5 .= K by A1,PBOOLE:3; hence a "/\" K = K; end; hence thesis by LATTICES:def 16; end; theorem Top EqRelLatt M = [|M,M|] proof set K = [|M,M|]; K is Equivalence_Relation of M by Th2; then reconsider K as Element of EqRelLatt M by MSUALG_5:def 5; now let a be Element of EqRelLatt M; reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5; A1: now let i be object; A2: ex K1 be ManySortedRelation of M st K1 = K9 (\/) a9 & K9 "\/" a9 = EqCl K1 by MSUALG_5:def 4; assume A3: i in I; then reconsider i9 = i as Element of I; reconsider K2 = K9.i9, a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2; (K9 (\/) a9).i = K9.i \/ a9.i by A3,PBOOLE:def 4 .= [:M.i,M.i:] \/ a9.i by A3,PBOOLE:def 16 .= nabla M.i \/ a2 by EQREL_1:def 1 .= nabla M.i by EQREL_1:1 .= [:M.i,M.i:] by EQREL_1:def 1 .= K9.i by A3,PBOOLE:def 16; hence (K9 "\/" a9).i = EqCl K2 by A2,MSUALG_5:def 3 .= K9.i by MSUALG_5:2; end; thus K "\/" a = (the L_join of EqRelLatt M).(K,a) by LATTICES:def 1 .= K9 "\/" a9 by MSUALG_5:def 5 .= K by A1,PBOOLE:3; hence a "\/" K = K; end; hence thesis by LATTICES:def 17; end; theorem Th5: for X be Subset of EqRelLatt M holds X is SubsetFamily of [|M,M|] proof let X be Subset of EqRelLatt M; now let x be object; assume x in the carrier of EqRelLatt M; then reconsider x9 = x as Equivalence_Relation of M by MSUALG_5:def 5; now let i be object; assume i in I; then reconsider i9 = i as Element of I; x9.i9 c= [:M.i9,M.i9:]; hence x9.i c= [|M,M|].i by PBOOLE:def 16; end; then x9 c= [|M,M|] by PBOOLE:def 2; then x9 is ManySortedSubset of [|M,M|] by PBOOLE:def 18; hence x in Bool [|M,M|] by CLOSURE2:def 1; end; then the carrier of EqRelLatt M c= Bool [|M,M|]; then bool the carrier of EqRelLatt M c= bool Bool [|M,M|] by ZFMISC_1:67; hence thesis; end; theorem Th6: for a,b be Element of EqRelLatt M, A,B be Equivalence_Relation of M st a = A & b = B holds a [= b iff A c= B proof let a,b be Element of EqRelLatt M; let A,B be Equivalence_Relation of M; assume that A1: a = A and A2: b = B; thus a [= b implies A c= B proof assume A3: a [= b; A (/\) B = (the L_meet of EqRelLatt M).(A,B) by MSUALG_5:def 5 .= a "/\" b by A1,A2,LATTICES:def 2 .= A by A1,A3,LATTICES:4; hence thesis by PBOOLE:15; end; thus A c= B implies a [= b proof assume A4: A c= B; a "/\" b = (the L_meet of EqRelLatt M).(A,B) by A1,A2,LATTICES:def 2 .= A (/\) B by MSUALG_5:def 5 .= a by A1,A4,PBOOLE:23; hence thesis by LATTICES:4; end; end; theorem Th7: for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X for a,b be Equivalence_Relation of M st a = meet |:X1:| & b in X holds a c= b proof let X be Subset of EqRelLatt M; let X1 be SubsetFamily of [|M,M|] such that A1: X1 = X; let a,b be Equivalence_Relation of M such that A2: a = meet |:X1:| and A3: b in X; now reconsider b9 = b as Element of Bool [|M,M|] by A1,A3; let i be object; assume A4: i in I; then |:X1:|.i = { x.i where x is Element of Bool [|M,M|] : x in X1 } by A1,A3, CLOSURE2:14; then A5: b9.i in |:X1:|.i by A1,A3; then A6: for y being object st y in meet (|:X1:|.i) holds y in b.i by SETFAM_1:def 1; ex Q be Subset-Family of ([|M,M|].i) st Q = |:X1:|.i & meet |:X1:|.i = Intersect Q by A4,MSSUBFAM:def 1; then a.i = meet (|:X1:|.i) by A2,A5,SETFAM_1:def 9; hence a.i c= b.i by A6; end; hence thesis by PBOOLE:def 2; end; theorem Th8: for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X & X is non empty holds meet |:X1:| is Equivalence_Relation of M proof let X be Subset of EqRelLatt M; let X1 be SubsetFamily of [|M,M|]; set a = meet |:X1:|; now let i be set; assume A1: i in I; a c= [|M,M|] by PBOOLE:def 18; then a.i c= [|M,M|].i by A1,PBOOLE:def 2; hence a.i is Relation of M.i by A1,PBOOLE:def 16; end; then reconsider a as ManySortedRelation of M by MSUALG_4:def 1; assume that A2: X1 = X and A3: X is non empty; now reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2,A3; let i be set, R be Relation of M.i; assume that A4: i in I and A5: a.i = R; reconsider i9 = i as Element of I by A4; reconsider b = |:X1:|.i9 as Subset-Family of [:M.i,M.i:] by PBOOLE:def 16; consider Q be Subset-Family of ([|M,M|].i) such that A6: Q = |:X1:|.i and A7: R = Intersect Q by A4,A5,MSSUBFAM:def 1; reconsider Q as Subset-Family of [:M.i,M.i:] by A4,PBOOLE:def 16; |:X19:| is non-empty; then A8: Q <> {} by A4,A6,PBOOLE:def 13; A9: |:X19:|.i = { x.i where x is Element of Bool [|M,M|] : x in X1 } by A4, CLOSURE2:14; now let Y; assume Y in b; then consider z be Element of Bool [|M,M|] such that A10: Y = z.i and A11: z in X by A2,A9; z c= [|M,M|] by PBOOLE:def 18; then z.i c= [|M,M|].i by A4,PBOOLE:def 2; then reconsider Y1 = Y as Relation of M.i by A4,A10,PBOOLE:def 16; z is Equivalence_Relation of M by A11,MSUALG_5:def 5; then Y1 is Equivalence_Relation of M.i by A4,A10,MSUALG_4:def 2; hence Y is Equivalence_Relation of M.i; end; then meet b is Equivalence_Relation of M.i by A6,A8,EQREL_1:11; hence R is Equivalence_Relation of M.i by A6,A7,A8,SETFAM_1:def 9; end; hence thesis by MSUALG_4:def 2; end; definition let L be non empty LattStr; redefine attr L is complete means for X being Subset of L ex a being Element of L st X is_less_than a & for b being Element of L st X is_less_than b holds a [= b; compatibility proof thus L is complete implies for X being Subset of L ex a being Element of L st X is_less_than a & for b being Element of L st X is_less_than b holds a [= b ; assume A1: for X being Subset of L ex a being Element of L st X is_less_than a & for b being Element of L st X is_less_than b holds a [= b; let X be set; defpred P[set] means $1 in X; set Y = { c where c is Element of L : P[c] }; Y is Subset of L from DOMAIN_1:sch 7; then consider p being Element of L such that A2: Y is_less_than p and A3: for r being Element of L st Y is_less_than r holds p [= r by A1; take p; thus X is_less_than p proof let q be Element of L; assume q in X; then q in Y; hence thesis by A2; end; let r be Element of L; assume A4: X is_less_than r; now let q be Element of L; assume q in Y; then ex v be Element of L st q = v & v in X; hence q [= r by A4; end; then Y is_less_than r; hence thesis by A3; end; end; theorem Th9: EqRelLatt M is complete proof for X being Subset of EqRelLatt M ex a being Element of EqRelLatt M st a is_less_than X & for b being Element of EqRelLatt M st b is_less_than X holds b [= a proof let X be Subset of EqRelLatt M; reconsider X1 = X as SubsetFamily of [|M,M|] by Th5; per cases; suppose A1: X is empty; take a = Top EqRelLatt M; for q be Element of EqRelLatt M st q in X holds a [= q by A1; hence a is_less_than X; let b be Element of EqRelLatt M; assume b is_less_than X; thus thesis by LATTICES:19; end; suppose A2: X is non empty; then reconsider a = meet |:X1:| as Equivalence_Relation of M by Th8; set a9 = a; reconsider a as Element of EqRelLatt M by MSUALG_5:def 5; take a; now let q be Element of EqRelLatt M; reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5; assume q in X; then a9 c= q9 by Th7; hence a [= q by Th6; end; hence a is_less_than X; now let b be Element of EqRelLatt M; reconsider b9 = b as Equivalence_Relation of M by MSUALG_5:def 5; assume A3: b is_less_than X; now reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2; let i be object; assume A4: i in I; then A5: ex Q be Subset-Family of ([|M,M|].i) st Q = |:X1:|.i & meet |:X1 :|.i = Intersect Q by MSSUBFAM:def 1; |:X19:| is non-empty; then A6: |:X1:|.i <> {} by A4,PBOOLE:def 13; now let Z be set; assume A7: Z in |:X1:|.i; |:X19:|.i = { x.i where x is Element of Bool [|M,M|] : x in X1 } by A4,CLOSURE2:14; then consider z be Element of Bool [|M,M|] such that A8: Z = z.i and A9: z in X1 by A7; reconsider z9 = z as Element of EqRelLatt M by A9; reconsider z99 = z9 as Equivalence_Relation of M by MSUALG_5:def 5; b [= z9 by A3,A9; then b9 c= z99 by Th6; hence b9.i c= Z by A4,A8,PBOOLE:def 2; end; then b9.i c= meet (|:X1:|.i) by A6,SETFAM_1:5; hence b9.i c= meet |:X1:|.i by A6,A5,SETFAM_1:def 9; end; then b9 c= meet |:X1:| by PBOOLE:def 2; hence b [= a by Th6; end; hence thesis; end; end; hence thesis by VECTSP_8:def 6; end; registration let I,M; cluster EqRelLatt M -> complete; coherence by Th9; end; theorem for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X & X is non empty for a,b be Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,EqRelLatt M) holds a = b proof let X be Subset of EqRelLatt M; let X1 be SubsetFamily of [|M,M|]; assume that A1: X1 = X and A2: X is non empty; let a,b be Equivalence_Relation of M; reconsider a9 = a as Element of EqRelLatt M by MSUALG_5:def 5; assume that A3: a = meet |:X1:| and A4: b = "/\" (X,EqRelLatt M); A5: now reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A1,A2; let c be Element of EqRelLatt M; reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5; reconsider S = |:X19:| as non-empty MSSubsetFamily of [|M,M|]; assume A6: c is_less_than X; now let Z1 be ManySortedSet of I; assume A7: Z1 in S; now let i be object; assume A8: i in I; then Z1.i in |:X1:|.i & |:X19:|.i = { x1.i where x1 is Element of Bool [|M,M|] : x1 in X1 } by A7,CLOSURE2:14,PBOOLE:def 1; then consider z be Element of Bool [|M,M|] such that A9: Z1.i = z.i and A10: z in X1; reconsider z9 = z as Element of EqRelLatt M by A1,A10; reconsider z1 = z9 as Equivalence_Relation of M by MSUALG_5:def 5; c [= z9 by A1,A6,A10; then c9 c= z1 by Th6; hence c9.i c= Z1.i by A8,A9,PBOOLE:def 2; end; hence c9 c= Z1 by PBOOLE:def 2; end; then c9 c= meet |:X1:| by MSSUBFAM:45; hence c [= a9 by A3,Th6; end; now let q be Element of EqRelLatt M; reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5; assume q in X; then a c= q9 by A1,A3,Th7; hence a9 [= q by Th6; end; then a9 is_less_than X; hence thesis by A4,A5,LATTICE3:34; end; begin :: SUBLATTICES INHERITING SUP'S AND INF'S definition let L be Lattice; let IT be SubLattice of L; attr IT is /\-inheriting means for X being Subset of IT holds "/\" (X ,L) in the carrier of IT; attr IT is \/-inheriting means for X being Subset of IT holds "\/" (X ,L) in the carrier of IT; end; theorem Th11: for L be Lattice, L9 be SubLattice of L, a,b be Element of L, a9 ,b9 be Element of L9 st a = a9 & b = b9 holds a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 proof let L be Lattice; let L9 be SubLattice of L; let a,b be Element of L; let a9,b9 be Element of L9; assume A1: a = a9 & b = b9; thus a "\/" b = (the L_join of L).(a,b) by LATTICES:def 1 .= ((the L_join of L)||the carrier of L9). [a9,b9] by A1,FUNCT_1:49 .= (the L_join of L9).(a9,b9) by NAT_LAT:def 12 .= a9 "\/" b9 by LATTICES:def 1; thus a "/\" b = (the L_meet of L).(a,b) by LATTICES:def 2 .= ((the L_meet of L)||the carrier of L9). [a9,b9] by A1,FUNCT_1:49 .= (the L_meet of L9).(a9,b9) by NAT_LAT:def 12 .= a9 "/\" b9 by LATTICES:def 2; end; theorem Th12: for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds a is_less_than X iff a9 is_less_than X proof let L be Lattice; let L9 be SubLattice of L; let X be Subset of L9; let a be Element of L; let a9 be Element of L9; assume A1: a = a9; thus a is_less_than X implies a9 is_less_than X proof assume A2: a is_less_than X; now let q9 be Element of L9; the carrier of L9 c= the carrier of L by NAT_LAT:def 12; then reconsider q = q9 as Element of L; assume q9 in X; then A3: a [= q by A2; a9 "/\" q9 = a "/\" q by A1,Th11 .= a9 by A1,A3,LATTICES:4; hence a9 [= q9 by LATTICES:4; end; hence thesis; end; thus a9 is_less_than X implies a is_less_than X proof assume A4: a9 is_less_than X; now let q be Element of L; assume A5: q in X; then reconsider q9 = q as Element of L9; A6: a9 [= q9 by A4,A5; a "/\" q = a9 "/\" q9 by A1,Th11 .= a by A1,A6,LATTICES:4; hence a [= q by LATTICES:4; end; hence thesis; end; end; theorem Th13: for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds X is_less_than a iff X is_less_than a9 proof let L be Lattice; let L9 be SubLattice of L; let X be Subset of L9; let a be Element of L; let a9 be Element of L9; assume A1: a = a9; thus X is_less_than a implies X is_less_than a9 proof assume A2: X is_less_than a; now let q9 be Element of L9; the carrier of L9 c= the carrier of L by NAT_LAT:def 12; then reconsider q = q9 as Element of L; assume q9 in X; then A3: q [= a by A2; q9 "/\" a9 = q "/\" a by A1,Th11 .= q9 by A3,LATTICES:4; hence q9 [= a9 by LATTICES:4; end; hence thesis; end; thus X is_less_than a9 implies X is_less_than a proof assume A4: X is_less_than a9; now let q be Element of L; assume A5: q in X; then reconsider q9 = q as Element of L9; A6: q9 [= a9 by A4,A5; q "/\" a = q9 "/\" a9 by A1,Th11 .= q by A6,LATTICES:4; hence q [= a by LATTICES:4; end; hence thesis; end; end; theorem Th14: for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting holds L9 is complete proof let L be complete Lattice; let L9 be SubLattice of L such that A1: L9 is /\-inheriting; for X being Subset of L9 ex a being Element of L9 st a is_less_than X & for b being Element of L9 st b is_less_than X holds b [= a proof let X be Subset of L9; set a = "/\" (X,L); reconsider a9 = a as Element of L9 by A1; take a9; a is_less_than X by LATTICE3:34; hence a9 is_less_than X by Th12; let b9 be Element of L9; the carrier of L9 c= the carrier of L by NAT_LAT:def 12; then reconsider b = b9 as Element of L; assume b9 is_less_than X; then b is_less_than X by Th12; then A2: b [= a by LATTICE3:39; b9 "/\" a9 = b "/\" a by Th11 .= b9 by A2,LATTICES:4; hence thesis by LATTICES:4; end; hence thesis by VECTSP_8:def 6; end; theorem Th15: for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting holds L9 is complete proof let L be complete Lattice; let L9 be SubLattice of L such that A1: L9 is \/-inheriting; for X being Subset of L9 ex a being Element of L9 st X is_less_than a & for b being Element of L9 st X is_less_than b holds a [= b proof let X be Subset of L9; set a = "\/" (X,L); reconsider a9 = a as Element of L9 by A1; take a9; X is_less_than a by LATTICE3:def 21; hence X is_less_than a9 by Th13; let b9 be Element of L9; the carrier of L9 c= the carrier of L by NAT_LAT:def 12; then reconsider b = b9 as Element of L; assume X is_less_than b9; then X is_less_than b by Th13; then A2: a [= b by LATTICE3:def 21; a9 "/\" b9 = a "/\" b by Th11 .= a9 by A2,LATTICES:4; hence thesis by LATTICES:4; end; hence thesis; end; registration let L be complete Lattice; cluster complete for SubLattice of L; existence proof reconsider L1 = L as SubLattice of L by NAT_LAT:15; take L1; thus thesis; end; end; registration let L be complete Lattice; cluster /\-inheriting -> complete for SubLattice of L; coherence by Th14; cluster \/-inheriting -> complete for SubLattice of L; coherence by Th15; end; theorem Th16: for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting for A9 be Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9) proof let L be complete Lattice; let L9 be SubLattice of L; assume A1: L9 is /\-inheriting; then reconsider L91 = L9 as complete SubLattice of L; let A9 be Subset of L9; set a = "/\" (A9,L); reconsider a9 = a as Element of L91 by A1; A2: now let c9 be Element of L91; the carrier of L91 c= the carrier of L by NAT_LAT:def 12; then reconsider c = c9 as Element of L; assume c9 is_less_than A9; then c is_less_than A9 by Th12; then A3: c [= a by LATTICE3:34; c9 "/\" a9 = c "/\" a by Th11 .= c9 by A3,LATTICES:4; hence c9 [= a9 by LATTICES:4; end; a is_less_than A9 by LATTICE3:34; then a9 is_less_than A9 by Th12; hence thesis by A2,LATTICE3:34; end; theorem Th17: for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting for A9 be Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9) proof let L be complete Lattice; let L9 be SubLattice of L; assume A1: L9 is \/-inheriting; then reconsider L91 = L9 as complete SubLattice of L; let A9 be Subset of L9; set a = "\/" (A9,L); reconsider a9 = a as Element of L91 by A1; A2: now let c9 be Element of L91; the carrier of L91 c= the carrier of L by NAT_LAT:def 12; then reconsider c = c9 as Element of L; assume A9 is_less_than c9; then A9 is_less_than c by Th13; then A3: a [= c by LATTICE3:def 21; a9 "/\" c9 = a "/\" c by Th11 .= a9 by A3,LATTICES:4; hence a9 [= c9 by LATTICES:4; end; A9 is_less_than a by LATTICE3:def 21; then A9 is_less_than a9 by Th13; hence thesis by A2,LATTICE3:def 21; end; theorem for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "/\" A = "/\" A9 by Th16; theorem for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "\/" A = "\/" A9 by Th17; begin :: SEGMENT OF REAL NUMBERS AS A COMPLETE LATTICE definition let r1,r2 such that A1: r1 <= r2; func RealSubLatt(r1,r2) -> strict Lattice means :Def4: the carrier of it = [.r1,r2.] & the L_join of it = maxreal||[.r1,r2.] & the L_meet of it = minreal ||[.r1,r2.]; existence proof r2 in { r : r1 <= r & r <= r2 } by A1; then reconsider A = [.r1,r2.] as non empty set by RCOMP_1:def 1; [:A,A:] c= [:REAL,REAL:] by ZFMISC_1:96; then reconsider Ma = maxreal||A, Mi = minreal||A as Function of [:A,A:],REAL by FUNCT_2:32; A2: dom Mi = [:A,A:] by FUNCT_2:def 1; A3: now let x be object; assume A4: x in dom Mi; then consider x1,x2 be object such that A5: x = [x1,x2] by RELAT_1:def 1; x2 in A by A4,A5,ZFMISC_1:87; then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then consider y2 be Real such that A6: x2 = y2 and A7: r1 <= y2 & y2 <= r2; reconsider y2 as Real; x1 in A by A4,A5,ZFMISC_1:87; then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then consider y1 be Real such that A8: x1 = y1 and A9: r1 <= y1 & y1 <= r2; reconsider y1 as Real; Mi.x = minreal.(x1,x2) by A4,A5,FUNCT_1:49 .= min(y1,y2) by A8,A6,REAL_LAT:def 1; then Mi.x = y1 or Mi.x = y2 by XXREAL_0:15; then Mi.x in { r : r1 <= r & r <= r2 } by A9,A7; hence Mi.x in A by RCOMP_1:def 1; end; A10: now let x be object; assume A11: x in dom Ma; then consider x1,x2 be object such that A12: x = [x1,x2] by RELAT_1:def 1; x2 in A by A11,A12,ZFMISC_1:87; then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then consider y2 be Real such that A13: x2 = y2 and A14: r1 <= y2 & y2 <= r2; reconsider y2 as Real; x1 in A by A11,A12,ZFMISC_1:87; then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then consider y1 be Real such that A15: x1 = y1 and A16: r1 <= y1 & y1 <= r2; reconsider y1 as Real; Ma.x = maxreal.(x1,x2) by A11,A12,FUNCT_1:49 .= max(y1,y2) by A15,A13,REAL_LAT:def 2; then Ma.x = y1 or Ma.x = y2 by XXREAL_0:16; then Ma.x in { r : r1 <= r & r <= r2 } by A16,A14; hence Ma.x in A by RCOMP_1:def 1; end; reconsider Mi as BinOp of A by A2,A3,FUNCT_2:3; dom Ma = [:A,A:] by FUNCT_2:def 1; then reconsider Ma as BinOp of A by A10,FUNCT_2:3; set R = Real_Lattice; set L9 = LattStr (# A, Ma, Mi #); reconsider L = L9 as non empty LattStr; A17: now let a,b be Element of L; thus a"\/"b = (the L_join of L).(a,b) by LATTICES:def 1 .= maxreal. [a,b] by FUNCT_1:49 .= maxreal.(a,b); thus a"/\"b = (the L_meet of L).(a,b) by LATTICES:def 2 .= minreal. [a,b] by FUNCT_1:49 .= minreal.(a,b); end; A18: for x being Element of A holds x is Element of R by REAL_LAT:def 3,XREAL_0:def 1; A19: now let p,q be Element of L; reconsider p9 = p, q9 = q as Element of R by A18; thus p"\/"q = maxreal.(p,q) by A17 .= maxreal.(q9,p9) by REAL_LAT:1 .= q"\/"p by A17; end; A20: now let p,q be Element of L; reconsider p9 = p, q9 = q as Element of R by A18; thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A17 .= minreal.(p9,maxreal.(p9,q9)) by A17 .= p by REAL_LAT:6; end; A21: now let p,q be Element of L; reconsider p9 = p, q9 = q as Element of R by A18; thus p"/\"q = minreal.(p,q) by A17 .= minreal.(q9,p9) by REAL_LAT:2 .= q"/\"p by A17; end; A22: now let p,q be Element of L; reconsider p9 = p, q9 = q as Element of R by A18; thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A17 .= maxreal.(minreal.(p9,q9),q9) by A17 .= q by REAL_LAT:5; end; A23: now let p,q,r be Element of L; reconsider p9 = p, q9 = q, r9 = r as Element of R by A18; thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A17 .= minreal.(p,minreal.(q,r)) by A17 .= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4 .= minreal.(p"/\"q,r) by A17 .= (p"/\"q)"/\"r by A17; end; now let p,q,r be Element of L; reconsider p9 = p, q9 = q, r9 = r as Element of R by A18; thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A17 .= maxreal.(p,maxreal.(q,r)) by A17 .= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3 .= maxreal.(p"\/"q,r) by A17 .= (p"\/"q)"\/"r by A17; end; then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A19,A22,A21,A23,A20, LATTICES:def 4,def 5,def 6,def 7,def 8,def 9; then reconsider L9 as strict Lattice; take L9; thus thesis; end; uniqueness; end; theorem Th20: for r1,r2 st r1 <= r2 holds RealSubLatt(r1,r2) is complete proof let r1,r2 such that A1: r1 <= r2; reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def 1; set A = [.r1,r2.]; set L9 = RealSubLatt(r1,r2); A2: the carrier of L9 = [.r1,r2.] by A1,Def4; A3: the L_meet of L9 = minreal||[.r1,r2.] by A1,Def4; now let X be Subset of L9; per cases; suppose A4: X is empty; thus ex a be Element of L9 st a is_less_than X & for b being Element of L9 st b is_less_than X holds b [= a proof r2 in { r : r1 <= r & r <= r2 } by A1; then reconsider a = r2 as Element of L9 by A2,RCOMP_1:def 1; take a; for q be Element of L9 st q in X holds a [= q by A4; hence a is_less_than X; let b be Element of L9; assume b is_less_than X; A5: b in [.r1,r2.] by A2; then reconsider b9 = b as Element of REAL; b in { r : r1 <= r & r <= r2 } by A5,RCOMP_1:def 1; then consider b1 be Real such that A6: b = b1 & r1 <= b1 & b1 <= r2; reconsider b1,r2 as Real; b "/\" a = (minreal||A).(b,a) by A3,LATTICES:def 2 .= minreal. [b,a] by A2,FUNCT_1:49 .= minreal.(b,a) .= min(b9,r2) by REAL_LAT:def 1 .= b by A6,XXREAL_0:def 9; hence thesis by LATTICES:4; end; end; suppose A7: X is non empty; X c= REAL by A2,XBOOLE_1:1; then reconsider X1 = X as non empty Subset of ExtREAL by A7,NUMBERS:31 ,XBOOLE_1:1; thus ex a be Element of L9 st a is_less_than X & for b being Element of L9 st b is_less_than X holds b [= a proof set g = the Element of X1; set A1 = inf X1; set LB = r1 - 1; LB is LowerBound of X1 proof let v be ExtReal; assume v in X1; then v in the carrier of L9; then v in { r : r1 <= r & r <= r2 } by A2,RCOMP_1:def 1; then consider w be Real such that A8: v = w and A9: r1 <= w and w <= r2; r1 - 1 <= r1 - 0 by XREAL_1:13; then r1 - 1 + r1 <= r1 + w by A9,XREAL_1:7; hence LB <= v by A8,XREAL_1:6; end; then A10: X1 is bounded_below; X <> {+infty} proof assume X = {+infty}; then +infty in X by TARSKI:def 1; hence contradiction by A2; end; then A11: A1 in REAL by A10,XXREAL_2:58; g in [.r1,r2.] by A2,TARSKI:def 3; then g in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then A12: ex w be Real st g = w & r1 <= w & w <= r2; A13: A1 is LowerBound of X1 by XXREAL_2:def 4; then A1 <= g by XXREAL_2:def 2; then consider A9,R29 be Real such that A14: A9 = A1 and A15: R29 = R2 & A9 <= R29 by A11,A12,XXREAL_0:2; now let v be ExtReal; assume v in X1; then v in A by A2; then v in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1; then ex w be Real st v = w & r1 <= w & w <= r2; hence R1 <= v; end; then R1 is LowerBound of X1 by XXREAL_2:def 2; then R1 <= A1 by XXREAL_2:def 4; then A9 in { r : r1 <= r & r <= r2 } by A14,A15; then reconsider a = A1 as Element of L9 by A2,A14,RCOMP_1:def 1; take a; a in [.r1,r2.] by A2; then reconsider a9 = a as Element of REAL; now let q be Element of L9; assume A16: q in X; q in [.r1,r2.] by A2; then reconsider q9 = q as Element of REAL; reconsider Q = q9 as R_eal by NUMBERS:31; A1 = a9; then A17: ex a1, q1 be Real st a1 = A1 & q1 = Q & a1 <= q1 by A13,A16, XXREAL_2:def 2; a "/\" q = (minreal||A).(a,q) by A3,LATTICES:def 2 .= minreal. [a,q] by A2,FUNCT_1:49 .= minreal.(a,q) .= min(a9,q9) by REAL_LAT:def 1 .= a by A17,XXREAL_0:def 9; hence a [= q by LATTICES:4; end; hence a is_less_than X; let b be Element of L9; b in [.r1,r2.] by A2; then reconsider b9 = b as Element of REAL; reconsider B = b9 as R_eal by NUMBERS:31; assume A18: b is_less_than X; now let h be ExtReal; assume A19: h in X; then reconsider h1 = h as Element of L9; h in [.r1,r2.] by A2,A19; then reconsider h9 = h as Real; A20: b [= h1 by A18,A19; min(b9,h9) = minreal.(b,h1) by REAL_LAT:def 1 .= (minreal||A). [b,h1] by A2,FUNCT_1:49 .= (minreal||A).(b,h1) .= b "/\" h1 by A3,LATTICES:def 2 .= b9 by A20,LATTICES:4; hence B <= h by XXREAL_0:def 9; end; then B is LowerBound of X1 by XXREAL_2:def 2; then A21: B <= A1 by XXREAL_2:def 4; b "/\" a = (minreal||A).(b,a) by A3,LATTICES:def 2 .= minreal. [b,a] by A2,FUNCT_1:49 .= minreal.(b,a) .= min(b9,a9) by REAL_LAT:def 1 .= b by A21,XXREAL_0:def 9; hence thesis by LATTICES:4; end; end; end; hence thesis by VECTSP_8:def 6; end; reconsider jj=1 as Real; reconsider jd=1/2 as Real; theorem Th21: ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) st L9 is \/-inheriting non /\-inheriting proof set B = {0,1} \/ ].1/2,1.[; set L = RealSubLatt(In(0,REAL),In(1,REAL)); set R = Real_Lattice; A1: B c= {0} \/ { x where x is Real: 1/2 < x & x <= 1 } proof let x1 be object; assume A2: x1 in B; now per cases by A2,XBOOLE_0:def 3; suppose x1 in {0,1}; then x1 = 0 or x1 = 1 by TARSKI:def 2; then x1 in {0} or x1 in { x where x is Real: 1/2 < x & x <= jj } by TARSKI:def 1; hence thesis by XBOOLE_0:def 3; end; suppose x1 in ].1/2,1.[; then x1 in { r : 1/2 < r & r < 1 } by RCOMP_1:def 2; then consider y be Real such that A3: x1 = y and A4: 1/2 < y & y < 1; y in { x where x is Real : 1/2 < x & x <= 1 } by A4; hence thesis by A3,XBOOLE_0:def 3; end; end; hence thesis; end; {0} \/ { x where x is Real : 1/2 < x & x <= 1 } c= B proof let x1 be object; assume A5: x1 in {0} \/ { x where x is Real : 1/2 < x & x <= 1 }; now per cases by A5,XBOOLE_0:def 3; suppose x1 in {0}; then x1 = 0 by TARSKI:def 1; then x1 in {0,1} by TARSKI:def 2; hence thesis by XBOOLE_0:def 3; end; suppose x1 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y be Real such that A6: x1 = y and A7: 1/2 < y and A8: y <= 1; y < 1 or y = 1 by A8,XXREAL_0:1; then y in { r : 1/2 < r & r < 1 } or y = 1 by A7; then y in ].1/2,1.[ or y in {0,1} by RCOMP_1:def 2,TARSKI:def 2; hence thesis by A6,XBOOLE_0:def 3; end; end; hence thesis; end; then A9: B = {0} \/ { x where x is Real : 1/2 < x & x <= 1 } by A1, XBOOLE_0:def 10; A10: 0 in { r : 0 <= r & r <= 1 }; then reconsider A = [.0,jj.] as non empty set by RCOMP_1:def 1; A11: the L_meet of L = minreal||[.0,jj.] by Def4; reconsider B as non empty set; A12: the L_join of L = maxreal||[.0,jj.] by Def4; A13: A = the carrier of L by Def4; then reconsider Ma = maxreal||A, Mi = minreal||A as BinOp of A by Def4; A14: now let x1 be object; assume A15: x1 in B; now per cases by A1,A15,XBOOLE_0:def 3; suppose x1 in {0}; then x1 = 0 by TARSKI:def 1; hence x1 in A by A10,RCOMP_1:def 1; end; suppose x1 in { x where x is Real: 1/2 < x & x <= 1 }; then ex y be Real st x1 = y & 1/2 < y & y <= 1; then x1 in { r : 0 <= r & r <= 1 }; hence x1 in A by RCOMP_1:def 1; end; end; hence x1 in A; end; then A16: B c= A; then A17: [:B,B:] c= [:A,A:] by ZFMISC_1:96; then reconsider ma = Ma||B, mi = Mi||B as Function of [:B,B:],A by FUNCT_2:32 ; A18: for x1 being Element of A holds x1 is Element of R by REAL_LAT:def 3,XREAL_0:def 1; A19: dom mi = [:B,B:] by FUNCT_2:def 1; A20: now let x9 be object; assume A21: x9 in dom mi; then consider x1,x2 be object such that A22: x9 = [x1,x2] by RELAT_1:def 1; A23: x2 in B by A21,A22,ZFMISC_1:87; A24: x1 in B by A21,A22,ZFMISC_1:87; now per cases by A1,A24,XBOOLE_0:def 3; suppose x1 in {0}; then A25: x1 = 0 by TARSKI:def 1; now per cases by A1,A23,XBOOLE_0:def 3; suppose x2 in {0}; then A26: x2 = 0 by TARSKI:def 1; mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49 .= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49 .= min(0,0) by A25,A26,REAL_LAT:def 1 .= 0; then mi.x9 in {0} by TARSKI:def 1; hence mi.x9 in B by A9,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y2 be Real such that A27: x2 = y2 and A28: 1/2 < y2 & y2 <= 1; reconsider y2 as Real; mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49 .= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49 .= min(0,y2) by A25,A27,REAL_LAT:def 1; then mi.x9 = 0 or mi.x9 = y2 by XXREAL_0:15; then mi.x9 in {0} or mi.x9 in { x where x is Real : 1/2 < x & x <= 1 } by A28,TARSKI:def 1; hence mi.x9 in B by A9,XBOOLE_0:def 3; end; end; hence mi.x9 in B; end; suppose x1 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y1 be Real such that A29: x1 = y1 and A30: 1/2 < y1 & y1 <= 1; reconsider y1 as Real; now per cases by A1,A23,XBOOLE_0:def 3; suppose x2 in {0}; then A31: x2 = 0 by TARSKI:def 1; mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49 .= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49 .= min(y1,0) by A29,A31,REAL_LAT:def 1; then mi.x9 = y1 or mi.x9 = 0 by XXREAL_0:15; then mi.x9 in { x where x is Real : 1/2 < x & x <= 1 } or mi.x9 in {0} by A30,TARSKI:def 1; hence mi.x9 in B by A9,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y2 be Real such that A32: x2 = y2 and A33: 1/2 < y2 & y2 <= 1; reconsider y2 as Real; mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49 .= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49 .= min(y1,y2) by A29,A32,REAL_LAT:def 1; then mi.x9 = y1 or mi.x9 = y2 by XXREAL_0:15; then mi.x9 in { x where x is Real : 1/2 < x & x <= 1 } by A30,A33; hence mi.x9 in B by A9,XBOOLE_0:def 3; end; end; hence mi.x9 in B; end; end; hence mi.x9 in B; end; A34: dom ma = [:B,B:] by FUNCT_2:def 1; A35: now let x9 be object; assume A36: x9 in dom ma; then consider x1,x2 be object such that A37: x9 = [x1,x2] by RELAT_1:def 1; A38: x2 in B by A36,A37,ZFMISC_1:87; A39: x1 in B by A36,A37,ZFMISC_1:87; now per cases by A1,A39,XBOOLE_0:def 3; suppose x1 in {0}; then A40: x1 = 0 by TARSKI:def 1; now per cases by A1,A38,XBOOLE_0:def 3; suppose x2 in {0}; then A41: x2 = 0 by TARSKI:def 1; ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49 .= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49 .= max(0,0) by A40,A41,REAL_LAT:def 2 .= 0; then ma.x9 in {0} by TARSKI:def 1; hence ma.x9 in B by A9,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y2 be Real such that A42: x2 = y2 and A43: 1/2 < y2 & y2 <= 1; reconsider y2 as Real; ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49 .= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49 .= max(0,y2) by A40,A42,REAL_LAT:def 2; then ma.x9 = 0 or ma.x9 = y2 by XXREAL_0:16; then ma.x9 in {0} or ma.x9 in { x where x is Real : 1/2 < x & x <= 1 } by A43,TARSKI:def 1; hence ma.x9 in B by A9,XBOOLE_0:def 3; end; end; hence ma.x9 in B; end; suppose x1 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y1 be Real such that A44: x1 = y1 and A45: 1/2 < y1 & y1 <= 1; reconsider y1 as Real; now per cases by A1,A38,XBOOLE_0:def 3; suppose x2 in {0}; then A46: x2 = 0 by TARSKI:def 1; ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49 .= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49 .= max(y1,0) by A44,A46,REAL_LAT:def 2; then ma.x9 = y1 or ma.x9 = 0 by XXREAL_0:16; then ma.x9 in { x where x is Real: 1/2 < x & x <= 1 } or ma.x9 in {0} by A45,TARSKI:def 1; hence ma.x9 in B by A9,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 1/2 < x & x <= 1 }; then consider y2 be Real such that A47: x2 = y2 and A48: 1/2 < y2 & y2 <= 1; reconsider y2 as Real; ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49 .= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49 .= max(y1,y2) by A44,A47,REAL_LAT:def 2; then ma.x9 = y1 or ma.x9 = y2 by XXREAL_0:16; then ma.x9 in { x where x is Real: 1/2 < x & x <= 1 } by A45,A48; hence ma.x9 in B by A9,XBOOLE_0:def 3; end; end; hence ma.x9 in B; end; end; hence ma.x9 in B; end; reconsider mi as BinOp of B by A19,A20,FUNCT_2:3; reconsider ma as BinOp of B by A34,A35,FUNCT_2:3; reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr; A49: now let a,b be Element of L9; thus a"\/"b = (the L_join of L9).(a,b) by LATTICES:def 1 .= (maxreal||A). [a,b] by FUNCT_1:49 .= maxreal.(a,b) by A17,FUNCT_1:49; thus a"/\"b = (the L_meet of L9).(a,b) by LATTICES:def 2 .= (minreal||A). [a,b] by FUNCT_1:49 .= minreal.(a,b) by A17,FUNCT_1:49; end; reconsider L as complete Lattice by Th20; A50: now let x1 be Element of B; now per cases by A9,XBOOLE_0:def 3; suppose x1 in {0}; then x1 = 0 by TARSKI:def 1; hence x1 is Element of L by A10,A13,RCOMP_1:def 1; end; suppose x1 in { x where x is Real : 1/2 < x & x <= 1 }; then ex y be Real st x1 = y & 1/2 < y & y <= 1; then x1 in { r : 0 <= r & r <= 1 }; hence x1 is Element of L by A13,RCOMP_1:def 1; end; end; hence x1 is Element of L; end; A51: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A50; reconsider p9, q9 as Element of R by A13,A18; thus p"\/"q = maxreal.(p,q) by A49 .= maxreal.(q9,p9) by REAL_LAT:1 .= q"\/"p by A49; end; A52: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A50; reconsider p9, q9 as Element of R by A13,A18; thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A49 .= minreal.(p9,maxreal.(p9,q9)) by A49 .= p by REAL_LAT:6; end; A53: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A50; reconsider p9, q9 as Element of R by A13,A18; thus p"/\"q = minreal.(p,q) by A49 .= minreal.(q9,p9) by REAL_LAT:2 .= q"/\"p by A49; end; A54: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A50; reconsider p9, q9 as Element of R by A13,A18; thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A49 .= maxreal.(minreal.(p9,q9),q9) by A49 .= q by REAL_LAT:5; end; A55: now let p,q,r be Element of L9; reconsider p9 = p, q9 = q, r9 = r as Element of L by A50; reconsider p9, q9, r9 as Element of R by A13,A18; thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A49 .= minreal.(p,minreal.(q,r)) by A49 .= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4 .= minreal.(p"/\"q,r) by A49 .= (p"/\"q)"/\"r by A49; end; now let p,q,r be Element of L9; reconsider p9 = p, q9 = q, r9 = r as Element of L by A50; reconsider p9, q9, r9 as Element of R by A13,A18; thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A49 .= maxreal.(p,maxreal.(q,r)) by A49 .= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3 .= maxreal.(p"\/"q,r) by A49 .= (p"\/"q)"\/"r by A49; end; then L9 is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A51,A54,A53,A55,A52, LATTICES:def 4,def 5,def 6,def 7,def 8,def 9; then reconsider L9 as Lattice; reconsider L9 as SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) by A13,A12,A11,A16, NAT_LAT:def 12; take L9; now let X be Subset of L9; thus "\/" (X,L) in the carrier of L9 proof 0 in { r : 0 <= r & r <= 1 }; then reconsider w = 0 as Element of L by A13,RCOMP_1:def 1; A56: X is_less_than "\/" (X,L) by LATTICE3:def 21; "\/" (X,L) in [.0,1.] by A13; then "\/" (X,L) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider y be Real such that A57: y = "\/" (X,L) and 0 <= y and A58: y <= 1; reconsider y as Real; assume A59: not "\/" (X,L) in the carrier of L9; then not "\/" (X,L) in { x where x is Real : 1/2 < x & x <= 1 } by A9,XBOOLE_0:def 3; then A60: y <= 1/2 by A57,A58; now let z9 be object; assume A61: z9 in X; then reconsider z = z9 as Element of L9; reconsider z as Element of L by A13,A14; A62: z [= "\/" (X,L) by A56,A61; reconsider z1 = z as Real; reconsider z1 as Real; min(z1,y) = minreal.(z1,"\/" (X,L)) by A57,REAL_LAT:def 1 .= (minreal||A). [z,"\/" (X,L)] by A13,FUNCT_1:49 .= (minreal||A).(z,"\/" (X,L)) .= z "/\" "\/" (X,L) by A11,LATTICES:def 2 .= z1 by A62,LATTICES:4; then z1 <= y by XXREAL_0:def 9; then y + z1 <= 1/2 + y by A60,XREAL_1:7; then for v be Real holds not (z1 = v & 1/2 < v & v <= 1) by XREAL_1:6; then not z1 in { x where x is Real: 1/2 < x & x <= 1 }; hence z9 in {0} by A9,XBOOLE_0:def 3; end; then A63: X c= {0}; now per cases by A63,ZFMISC_1:33; suppose A64: X = {}; A65: now let r1 be Element of L; assume X is_less_than r1; r1 in [.0,1.] by A13; then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider e be Real such that A66: r1 = e and A67: 0 <= e and e <= 1; reconsider e as Real; w "/\" r1 = (minreal||A).(w,r1) by A11,LATTICES:def 2 .= minreal. [w,r1] by A13,FUNCT_1:49 .= minreal.(w,r1) .= min(0,e) by A66,REAL_LAT:def 1 .= w by A67,XXREAL_0:def 9; hence w [= r1 by LATTICES:4; end; for q be Element of L st q in X holds q [= w by A64; then X is_less_than w; then "\/" (X,L) = w by A65,LATTICE3:def 21; then "\/" (X,L) in {0} by TARSKI:def 1; hence contradiction by A9,A59,XBOOLE_0:def 3; end; suppose X = {0}; then "\/" (X,L) = w by LATTICE3:42; then "\/" (X,L) in {0} by TARSKI:def 1; hence contradiction by A9,A59,XBOOLE_0:def 3; end; end; hence contradiction; end; end; hence L9 is \/-inheriting; now 1/2 in { x where x is Real: 0 <= x & x <= 1 }; then reconsider z = 1/2 as Element of L by A13,RCOMP_1:def 1; set X = { x where x is Real : 1/2 < x & x <= 1 }; for y be Real holds not ( y = 1/2 & 1/2 < y & y <= 1); then A68: ( not 1/2 in {0})& not 1/2 in { x where x is Real: 1/2 < x & x <= 1 } by TARSKI:def 1; for x1 be object st x1 in { x where x is Real: 1/2 < x & x <= 1 } holds x1 in B by A9,XBOOLE_0:def 3; then reconsider X as Subset of L9 by TARSKI:def 3; take X; A69: now let b be Element of L; b in A by A13; then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider b9 be Real such that A70: b = b9 and A71: 0 <= b9 and A72: b9 <= 1; reconsider b9 as Real; assume A73: b is_less_than X; A74: b9 <= 1/2 proof assume A75: 1/2 < b9; then b9 in X by A72; then A76: b = "/\" (X,L) by A70,A73,LATTICE3:41; 1/2 + b9 < b9 + b9 by A75,XREAL_1:6; then A77: (1/2 + b9)/2 < (b9 + b9)/2 by XREAL_1:74; then (1/2 + b9)/2 + b9 <= b9 + 1 by A72,XREAL_1:7; then A78: (1/2 + b9)/2 <= 1 by XREAL_1:6; then (1/2 + b9)/2 in { r : 0 <= r & r <= 1} by A71; then reconsider c = (1/2 + b9)/2 as Element of L by A13,RCOMP_1:def 1; reconsider cc = c as Real; 1/2 + 1/2 < b9 + 1/2 by A75,XREAL_1:6; then 1/2 < (1/2 + b9)/2 by XREAL_1:74; then (1/2 + b9)/2 in X by A78; then b [= c by A76,LATTICE3:38; then b9 = b "/\" c by A70,LATTICES:4 .= (minreal||A).(b,c) by A11,LATTICES:def 2 .= minreal. [b,c] by A13,FUNCT_1:49 .= minreal.(b,cc) .= min(b9,(1/2 + b9)/2) by A70,REAL_LAT:def 1; hence contradiction by A77,XXREAL_0:def 9; end; b "/\" z = (minreal||A).(b,z) by A11,LATTICES:def 2 .= minreal. [b,z] by A13,FUNCT_1:49 .= minreal.(b,z) .= min(b9,jd) by A70,REAL_LAT:def 1 .= b by A70,A74,XXREAL_0:def 9; hence b [= z by LATTICES:4; end; now let q be Element of L; assume q in X; then A79: ex y be Real st q = y & 1/2 < y & y <= 1; q in A by A13; then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider q9 be Real such that A80: q = q9 and 0 <= q9 and q9 <= 1; reconsider q9 as Real; z "/\" q = (minreal||A).(z,q) by A11,LATTICES:def 2 .= minreal. [z,q] by A13,FUNCT_1:49 .= minreal.(z,q) .= min(jd,q9) by A80,REAL_LAT:def 1 .= z by A80,A79,XXREAL_0:def 9; hence z [= q by LATTICES:4; end; then z is_less_than X; then "/\"(X,L) = jd by A69,LATTICE3:34; hence not "/\" (X,L) in the carrier of L9 by A1,A68,XBOOLE_0:def 3; end; hence thesis; end; theorem ex L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting non /\-inheriting proof reconsider L = RealSubLatt(In(0,REAL),In(1,REAL)) as complete Lattice by Th20; take L; thus thesis by Th21; end; theorem Th23: ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) st L9 is /\-inheriting non \/-inheriting proof set B = {0,1} \/ ].0,1/2.[; set L = RealSubLatt(In(0,REAL),In(1,REAL)); set R = Real_Lattice; A1: B c= {1} \/ { x where x is Real : 0 <= x & x < 1/2 } proof let x1 be object; assume A2: x1 in B; now per cases by A2,XBOOLE_0:def 3; suppose x1 in {0,1}; then x1 = 0 or x1 = 1 by TARSKI:def 2; then x1 in {1} or x1 in { x where x is Real : 0 <= x & x < 1/2 } by TARSKI:def 1; hence thesis by XBOOLE_0:def 3; end; suppose x1 in ].0,1/2.[; then x1 in { r : 0 < r & r < 1/2 } by RCOMP_1:def 2; then consider y be Real such that A3: x1 = y and A4: 0 < y & y < 1/2; y in { x where x is Real: 0 <= x & x < 1/2 } by A4; hence thesis by A3,XBOOLE_0:def 3; end; end; hence thesis; end; {1} \/ { x where x is Real : 0 <= x & x < 1/2 } c= B proof let x1 be object; assume A5: x1 in {1} \/ { x where x is Real : 0 <= x & x < 1/2 }; now per cases by A5,XBOOLE_0:def 3; suppose x1 in {1}; then x1 = 1 by TARSKI:def 1; then x1 in {0,1} by TARSKI:def 2; hence thesis by XBOOLE_0:def 3; end; suppose x1 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y be Real such that A6: x1 = y and A7: 0 <= y & y < 1/2; y in { r : 0 < r & r < 1/2 } or y = 0 by A7; then y in ].0,1/2.[ or y in {0,1} by RCOMP_1:def 2,TARSKI:def 2; hence thesis by A6,XBOOLE_0:def 3; end; end; hence thesis; end; then A8: B = {1} \/ { x where x is Real: 0 <= x & x < 1/2 } by A1, XBOOLE_0:def 10; A9: 1 in { r : 0 <= r & r <= 1 }; then reconsider A = [.0,1.] as non empty set by RCOMP_1:def 1; A10: for x1 being Element of A holds x1 is Element of R by REAL_LAT:def 3,XREAL_0:def 1; reconsider B as non empty set; A11: the L_meet of L = minreal||[.0,1.] by Def4; set Ma = maxreal||A, Mi = minreal||A; A12: the L_join of L = maxreal||[.0,1.] by Def4; A13: A = the carrier of L by Def4; then reconsider Ma, Mi as BinOp of A by Def4; A14: now let x1 be object; assume A15: x1 in B; now per cases by A1,A15,XBOOLE_0:def 3; suppose x1 in {1}; then x1 = 1 by TARSKI:def 1; hence x1 in A by A9,RCOMP_1:def 1; end; suppose x1 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y be Real such that A16: x1 = y & 0 <= y and A17: y < 1/2; y + 1/2 <= 1/2 + 1 by A17,XREAL_1:7; then y <= 1 by XREAL_1:6; then x1 in { r : 0 <= r & r <= 1 } by A16; hence x1 in A by RCOMP_1:def 1; end; end; hence x1 in A; end; then A18: B c= A; then A19: [:B,B:] c= [:A,A:] by ZFMISC_1:96; then reconsider ma = Ma||B, mi = Mi||B as Function of [:B,B:],A by FUNCT_2:32 ; A20: dom ma = [:B,B:] by FUNCT_2:def 1; A21: now let x9 be object; assume A22: x9 in dom ma; then consider x1,x2 be object such that A23: x9 = [x1,x2] by RELAT_1:def 1; A24: x2 in B by A22,A23,ZFMISC_1:87; A25: x1 in B by A22,A23,ZFMISC_1:87; now per cases by A1,A25,XBOOLE_0:def 3; suppose x1 in {1}; then A26: x1 = 1 by TARSKI:def 1; now per cases by A1,A24,XBOOLE_0:def 3; suppose x2 in {1}; then A27: x2 = 1 by TARSKI:def 1; ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49 .= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49 .= max(jj,jj) by A26,A27,REAL_LAT:def 2 .= 1; then ma.x9 in {1} by TARSKI:def 1; hence ma.x9 in B by A8,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y2 be Real such that A28: x2 = y2 and A29: 0 <= y2 & y2 < 1/2; reconsider y2 as Real; ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49 .= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49 .= max(jj,y2) by A26,A28,REAL_LAT:def 2; then ma.x9 = 1 or ma.x9 = y2 by XXREAL_0:16; then ma.x9 in {1} or ma.x9 in { x where x is Real : 0 <= x & x < 1/2 } by A29,TARSKI:def 1; hence ma.x9 in B by A8,XBOOLE_0:def 3; end; end; hence ma.x9 in B; end; suppose x1 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y1 be Real such that A30: x1 = y1 and A31: 0 <= y1 & y1 < 1/2; reconsider y1 as Real; now per cases by A1,A24,XBOOLE_0:def 3; suppose x2 in {1}; then A32: x2 = 1 by TARSKI:def 1; ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49 .= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49 .= max(y1,jj) by A30,A32,REAL_LAT:def 2; then ma.x9 = y1 or ma.x9 = 1 by XXREAL_0:16; then ma.x9 in { x where x is Real : 0 <= x & x < 1/2 } or ma.x9 in {1} by A31,TARSKI:def 1; hence ma.x9 in B by A8,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y2 be Real such that A33: x2 = y2 and A34: 0 <= y2 & y2 < 1/2; reconsider y2 as Real; ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49 .= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49 .= max(y1,y2) by A30,A33,REAL_LAT:def 2; then ma.x9 = y1 or ma.x9 = y2 by XXREAL_0:16; then ma.x9 in { x where x is Real : 0 <= x & x < 1/2 } by A31,A34; hence ma.x9 in B by A8,XBOOLE_0:def 3; end; end; hence ma.x9 in B; end; end; hence ma.x9 in B; end; A35: dom mi = [:B,B:] by FUNCT_2:def 1; A36: now let x9 be object; assume A37: x9 in dom mi; then consider x1,x2 be object such that A38: x9 = [x1,x2] by RELAT_1:def 1; A39: x2 in B by A37,A38,ZFMISC_1:87; A40: x1 in B by A37,A38,ZFMISC_1:87; now per cases by A1,A40,XBOOLE_0:def 3; suppose x1 in {1}; then A41: x1 = 1 by TARSKI:def 1; now per cases by A1,A39,XBOOLE_0:def 3; suppose x2 in {1}; then A42: x2 = 1 by TARSKI:def 1; mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49 .= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49 .= min(jj,jj) by A41,A42,REAL_LAT:def 1 .= 1; then mi.x9 in {1} by TARSKI:def 1; hence mi.x9 in B by A8,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y2 be Real such that A43: x2 = y2 and A44: 0 <= y2 & y2 < 1/2; reconsider y2 as Real; mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49 .= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49 .= min(jj,y2) by A41,A43,REAL_LAT:def 1; then mi.x9 = 1 or mi.x9 = y2 by XXREAL_0:15; then mi.x9 in {1} or mi.x9 in { x where x is Real : 0 <= x & x < 1/2 } by A44,TARSKI:def 1; hence mi.x9 in B by A8,XBOOLE_0:def 3; end; end; hence mi.x9 in B; end; suppose x1 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y1 be Real such that A45: x1 = y1 and A46: 0 <= y1 & y1 < 1/2; reconsider y1 as Real; now per cases by A1,A39,XBOOLE_0:def 3; suppose x2 in {1}; then A47: x2 = 1 by TARSKI:def 1; mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49 .= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49 .= min(y1,jj) by A45,A47,REAL_LAT:def 1; then mi.x9 = y1 or mi.x9 = 1 by XXREAL_0:15; then mi.x9 in { x where x is Real : 0 <= x & x < 1/2 } or mi.x9 in {1} by A46,TARSKI:def 1; hence mi.x9 in B by A8,XBOOLE_0:def 3; end; suppose x2 in { x where x is Real : 0 <= x & x < 1/2 }; then consider y2 be Real such that A48: x2 = y2 and A49: 0 <= y2 & y2 < 1/2; reconsider y2 as Real; mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49 .= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49 .= min(y1,y2) by A45,A48,REAL_LAT:def 1; then mi.x9 = y1 or mi.x9 = y2 by XXREAL_0:15; then mi.x9 in { x where x is Real : 0 <= x & x < 1/2 } by A46,A49; hence mi.x9 in B by A8,XBOOLE_0:def 3; end; end; hence mi.x9 in B; end; end; hence mi.x9 in B; end; reconsider L as complete Lattice by Th20; reconsider mi as BinOp of B by A35,A36,FUNCT_2:3; reconsider ma as BinOp of B by A20,A21,FUNCT_2:3; reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr; A50: now let a,b be Element of L9; thus a"\/"b = (the L_join of L9).(a,b) by LATTICES:def 1 .= (maxreal||A). [a,b] by FUNCT_1:49 .= maxreal.(a,b) by A19,FUNCT_1:49; thus a"/\"b = (the L_meet of L9).(a,b) by LATTICES:def 2 .= (minreal||A). [a,b] by FUNCT_1:49 .= minreal.(a,b) by A19,FUNCT_1:49; end; A51: now let x1 be Element of B; per cases by A8,XBOOLE_0:def 3; suppose x1 in {1}; then x1 = 1 by TARSKI:def 1; hence x1 is Element of L by A9,A13,RCOMP_1:def 1; end; suppose x1 in { x where x is Real: 0 <= x & x < 1/2 }; then consider y be Real such that A52: x1 = y & 0 <= y and A53: y < 1/2; y + 1/2 <= 1/2 + 1 by A53,XREAL_1:7; then y <= 1 by XREAL_1:6; then x1 in { r : 0 <= r & r <= 1 } by A52; hence x1 is Element of L by A13,RCOMP_1:def 1; end; end; A54: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A51; reconsider p9, q9 as Element of R by A13,A10; thus p"\/"q = maxreal.(p,q) by A50 .= maxreal.(q9,p9) by REAL_LAT:1 .= q"\/"p by A50; end; A55: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A51; reconsider p9, q9 as Element of R by A13,A10; thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A50 .= minreal.(p9,maxreal.(p9,q9)) by A50 .= p by REAL_LAT:6; end; A56: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A51; reconsider p9, q9 as Element of R by A13,A10; thus p"/\"q = minreal.(p,q) by A50 .= minreal.(q9,p9) by REAL_LAT:2 .= q"/\"p by A50; end; A57: now let p,q be Element of L9; reconsider p9 = p, q9 = q as Element of L by A51; reconsider p9, q9 as Element of R by A13,A10; thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A50 .= maxreal.(minreal.(p9,q9),q9) by A50 .= q by REAL_LAT:5; end; A58: now let p,q,r be Element of L9; reconsider p9 = p, q9 = q, r9 = r as Element of L by A51; reconsider p9, q9, r9 as Element of R by A13,A10; thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A50 .= minreal.(p,minreal.(q,r)) by A50 .= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4 .= minreal.(p"/\"q,r) by A50 .= (p"/\"q)"/\"r by A50; end; now let p,q,r be Element of L9; reconsider p9 = p, q9 = q, r9 = r as Element of L by A51; reconsider p9, q9, r9 as Element of R by A13,A10; thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A50 .= maxreal.(p,maxreal.(q,r)) by A50 .= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3 .= maxreal.(p"\/"q,r) by A50 .= (p"\/"q)"\/"r by A50; end; then L9 is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A54,A57,A56,A58,A55, LATTICES:def 4,def 5,def 6,def 7,def 8,def 9; then reconsider L9 as Lattice; reconsider L9 as SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) by A13,A12,A11,A18, NAT_LAT:def 12; take L9; now let X be Subset of L9; thus "/\" (X,L) in the carrier of L9 proof 1 in { r : 0 <= r & r <= 1 }; then reconsider w = 1 as Element of L by A13,RCOMP_1:def 1; A59: "/\" (X,L) is_less_than X by LATTICE3:34; "/\" (X,L) in [.0,1.] by A13; then "/\" (X,L) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider y be Real such that A60: y = "/\" (X,L) and A61: 0 <= y and y <= 1; reconsider y as Real; assume A62: not "/\" (X,L) in the carrier of L9; then not "/\" (X,L) in { x where x is Real : 0 <= x & x < 1/ 2 } by A8,XBOOLE_0:def 3; then A63: 1/2 <= y by A60,A61; now let z9 be object; assume A64: z9 in X; then reconsider z = z9 as Element of L9; reconsider z as Element of L by A13,A14; A65: "/\" (X,L) [= z by A59,A64; reconsider z1 = z as Real; reconsider z1 as Real; min(z1,y) = minreal.(z1,"/\" (X,L)) by A60,REAL_LAT:def 1 .= (minreal||A). [z,"/\" (X,L)] by A13,FUNCT_1:49 .= (minreal||A).(z,"/\" (X,L)) .= z "/\" "/\" (X,L) by A11,LATTICES:def 2 .= y by A60,A65,LATTICES:4; then y <= z1 by XXREAL_0:def 9; then y + 1/2 <= z1 + y by A63,XREAL_1:7; then for v be Real holds not (z1 = v & 0 <= v & v < 1/2) by XREAL_1:6; then not z1 in { x where x is Real : 0 <= x & x < 1/2 }; hence z9 in {1} by A8,XBOOLE_0:def 3; end; then A66: X c= {1}; now per cases by A66,ZFMISC_1:33; suppose A67: X = {}; A68: now let r1 be Element of L; assume r1 is_less_than X; r1 in [.0,1.] by A13; then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider e be Real such that A69: r1 = e and 0 <= e and A70: e <= 1; reconsider e as Real; r1 "/\" w = (minreal||A).(r1,w) by A11,LATTICES:def 2 .= minreal. [r1,w] by A13,FUNCT_1:49 .= minreal.(r1,w) .= min(e,jj) by A69,REAL_LAT:def 1 .= r1 by A69,A70,XXREAL_0:def 9; hence r1 [= w by LATTICES:4; end; for q be Element of L st q in X holds w [= q by A67; then w is_less_than X; then "/\" (X,L) = w by A68,LATTICE3:34; then "/\" (X,L) in {1} by TARSKI:def 1; hence contradiction by A8,A62,XBOOLE_0:def 3; end; suppose X = {1}; then "/\" (X,L) = w by LATTICE3:42; then "/\" (X,L) in {1} by TARSKI:def 1; hence contradiction by A8,A62,XBOOLE_0:def 3; end; end; hence contradiction; end; end; hence L9 is /\-inheriting; now 1/2 in { x where x is Real : 0 <= x & x <= 1 }; then reconsider z = 1/2 as Element of L by A13,RCOMP_1:def 1; set X = { x where x is Real: 0 <= x & x < 1/2 }; for y be Real holds not ( y = 1/2 & 0 <= y & y < 1/2); then A71: ( not 1/2 in {1})& not 1/2 in { x where x is Real : 0 <= x & x < 1/ 2 } by TARSKI:def 1; for x1 be object st x1 in { x where x is Real : 0 <= x & x < 1 / 2 } holds x1 in B by A8,XBOOLE_0:def 3; then reconsider X as Subset of L9 by TARSKI:def 3; take X; A72: now let b be Element of L; b in A by A13; then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider b9 be Real such that A73: b = b9 and A74: 0 <= b9 and A75: b9 <= 1; reconsider b9 as Real; assume A76: X is_less_than b; A77: 1/2 <= b9 proof 1/2 + b9 <= 1 + 1 by A75,XREAL_1:7; then (1/2 + b9)/2 <= (1 + 1)/2 by XREAL_1:72; then (1/2 + b9)/2 in { r : 0 <= r & r <= 1} by A74; then reconsider c = (1/2 + b9)/2 as Element of L by A13,RCOMP_1:def 1; reconsider cc = c as Real; assume A78: b9 < 1/2; then b9 + b9 < 1/2 + b9 by XREAL_1:6; then A79: (b9 + b9)/2 < (1/2 + b9)/2 by XREAL_1:74; b9 + 1/2 < 1/2 + 1/2 by A78,XREAL_1:6; then (1/2 + b9)/2 < 1/2 by XREAL_1:74; then A80: (jd + b9)/2 in X by A74; b9 in X by A74,A78; then b = "\/" (X,L) by A73,A76,LATTICE3:40; then c [= b by A80,LATTICE3:38; then (1/2 + b9)/2 = c "/\" b by LATTICES:4 .= (minreal||A).(c,b) by A11,LATTICES:def 2 .= minreal. [c,b] by A13,FUNCT_1:49 .= minreal.(cc,b) .= min((1/2 + b9)/2,b9) by A73,REAL_LAT:def 1; hence contradiction by A79,XXREAL_0:def 9; end; z "/\" b = (minreal||A).(z,b) by A11,LATTICES:def 2 .= minreal. [z,b] by A13,FUNCT_1:49 .= minreal.(z,b) .= min(jd,b9) by A73,REAL_LAT:def 1 .= z by A77,XXREAL_0:def 9; hence z [= b by LATTICES:4; end; now let q be Element of L; assume q in X; then A81: ex y be Real st q = y & 0 <= y & y < 1/2; q in A by A13; then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1; then consider q9 be Real such that A82: q = q9 and 0 <= q9 and q9 <= 1; reconsider q9 as Real; q "/\" z = (minreal||A).(q,z) by A11,LATTICES:def 2 .= minreal. [q,z] by A13,FUNCT_1:49 .= minreal.(q,z) .= min(q9,jd) by A82,REAL_LAT:def 1 .= q by A82,A81,XXREAL_0:def 9; hence q [= z by LATTICES:4; end; then X is_less_than z; then "\/" (X,L) = 1/2 by A72,LATTICE3:def 21; hence not "\/" (X,L) in the carrier of L9 by A1,A71,XBOOLE_0:def 3; end; hence thesis; end; theorem ex L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting non \/-inheriting proof reconsider L = RealSubLatt(In(0,REAL),In(1,REAL)) as complete Lattice by Th20; take L; thus thesis by Th23; end;