:: The Lattice of Real Numbers. The Lattice of Real Functions :: by Marek Chmur :: :: Received May 22, 1990 :: Copyright (c) 1990-2018 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 REAL_1, BINOP_1, NUMBERS, FUNCT_1, XXREAL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, FUNCT_2, RELAT_1, REAL_LAT, MEMBERED, STRUCT_0, FUNCT_7; notations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, MEMBERED, STRUCT_0, LATTICES, BINOP_1, FUNCSDOM, RELAT_1, FUNCT_2; constructors SQUARE_1, LATTICES, FUNCSDOM, RELSET_1, MEMBERED, XXREAL_0; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, LATTICES, MEMBERED; requirements SUBSET, BOOLE; definitions LATTICES; equalities LATTICES; expansions LATTICES; theorems LATTICES, BINOP_1, FUNCT_2, FUNCOP_1, XXREAL_0, XREAL_0; schemes BINOP_1; begin :: LATTICE of REAL NUMBERS reserve x,y for Real; definition func minreal-> BinOp of REAL means :Def1: it.(x,y)=min(x,y); existence proof deffunc F(Real,Real) = In(min(\$1,\$2),REAL); consider o being BinOp of REAL such that A1:for a,b being Element of REAL holds o.(a,b) = F(a,b) from BINOP_1:sch 4; take o; let a,b be Real; reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1; o.(aa,bb) = F(aa,bb) by A1; hence thesis; end; uniqueness proof let f1,f2 be BinOp of REAL; assume that A2: f1.(x,y)=min(x,y) and A3: f2.(x,y)=min(x,y); for x,y being Element of REAL holds f1.(x,y)=f2.(x,y) proof let x,y be Element of REAL; f1.(x,y)=min(x,y) by A2; hence thesis by A3; end; hence thesis by BINOP_1:2; end; func maxreal-> BinOp of REAL means :Def2: it.(x,y)=max(x,y); existence proof deffunc F(Real,Real) = In(max(\$1,\$2),REAL); consider o being BinOp of REAL such that A4: for a,b being Element of REAL holds o.(a,b) = F(a,b) from BINOP_1:sch 4; take o; let a,b be Real; reconsider a,b as Element of REAL by XREAL_0:def 1; o.(a,b) = F(a,b) by A4; hence thesis; end; uniqueness proof let f1,f2 be BinOp of REAL; assume that A5: f1.(x,y)=max(x,y) and A6: f2.(x,y)=max(x,y); for x,y being Element of REAL holds f1.(x,y)=f2.(x,y) proof let x,y be Element of REAL; f1.(x,y)=max(x,y) by A5; hence thesis by A6; end; hence thesis by BINOP_1:2; end; end; definition func Real_Lattice -> strict LattStr equals LattStr (# REAL, maxreal, minreal #); coherence; end; registration cluster the carrier of Real_Lattice -> real-membered; coherence; end; registration cluster Real_Lattice -> non empty; coherence; end; reserve a,b,c for Element of Real_Lattice; registration let a,b be Element of Real_Lattice; identify a "\/" b with max(a,b); compatibility by Def2; identify a "/\" b with min(a,b); compatibility by Def1; end; Lm1: a"\/"(b"\/"c) = (a"\/"b)"\/"c by XXREAL_0:34; Lm2: (a"/\"b)"\/"b = b by XXREAL_0:36; Lm3: a"/\"(b"/\"c) = (a"/\"b)"/\"c by XXREAL_0:33; Lm4: a"/\"(a"\/"b) = a by XXREAL_0:35; registration cluster Real_Lattice -> Lattice-like; coherence proof Real_Lattice is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by Lm1,Lm2,Lm3,Lm4; hence thesis; end; end; Lm5: a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by XXREAL_0:38; reserve p,q,r for Element of Real_Lattice; theorem Th1: maxreal.(p,q) = maxreal.(q,p) proof thus maxreal.(p,q) = q"\/"p by LATTICES:def 1 .= maxreal.(q,p); end; theorem Th2: minreal.(p,q) = minreal.(q,p) proof thus minreal.(p,q) = q"/\"p by LATTICES:def 2 .= minreal.(q,p); end; theorem Th3: maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(q,r)),p) & maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,q)),r) & maxreal.(p,(maxreal.( q,r)))=maxreal.((maxreal.(q,p)),r) & maxreal.(p,(maxreal.(q,r)))=maxreal.(( maxreal.(r,p)),q) & maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,q)),p) & maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,r)),q) proof set s=q"\/"r; thus A1: maxreal.(p,(maxreal.(q,r))) = s"\/"p by LATTICES:def 1 .= maxreal.((maxreal.(q,r)),p); thus maxreal.(p,(maxreal.(q,r))) = p"\/"s .= (p"\/"q)"\/"r by XXREAL_0:34 .= maxreal.(maxreal.(p,q),r); thus maxreal.(p,(maxreal.(q,r))) = p"\/"s .= (q"\/"p)"\/"r by XXREAL_0:34 .= maxreal.(maxreal.(q,p),r); thus A2: maxreal.(p,(maxreal.(q,r))) = p"\/"(q"\/"r) .= (r"\/"p)"\/"q by XXREAL_0:34 .= maxreal.(maxreal.(r,p),q); thus maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,q)),p) by A1,Th1; thus thesis by A2,Th1; end; theorem Th4: minreal.(p,(minreal.(q,r)))=minreal.((minreal.(q,r)),p) & minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,q)),r) & minreal.(p,(minreal.( q,r)))=minreal.((minreal.(q,p)),r) & minreal.(p,(minreal.(q,r)))=minreal.(( minreal.(r,p)),q) & minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,q)),p) & minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,r)),q) proof set s=q"/\"r; thus A1: minreal.(p,(minreal.(q,r))) = s"/\"p by LATTICES:def 2 .= minreal.((minreal.(q,r)),p); thus minreal.(p,(minreal.(q,r))) = p"/\"s .= (p"/\"q)"/\"r by XXREAL_0:33 .= minreal.(minreal.(p,q),r); thus minreal.(p,(minreal.(q,r))) = p"/\"s .= (q"/\"p)"/\"r by XXREAL_0:33 .= minreal.(minreal.(q,p),r); thus A2: minreal.(p,(minreal.(q,r))) = p"/\"(q"/\"r) .= (r"/\"p)"/\"q by XXREAL_0:33 .= minreal.(minreal.(r,p),q); thus minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,q)),p) by A1,Th2; thus thesis by A2,Th2; end; theorem Th5: maxreal.(minreal.(p,q),q)=q & maxreal.(q,minreal.(p,q))=q & maxreal.(q,minreal.(q,p))=q & maxreal.(minreal.(q,p),q)=q proof set s=p"/\"q; thus A1: maxreal.(minreal.(p,q),q) =s"\/"q .=q by XXREAL_0:36; thus maxreal.(q,minreal.(p,q)) =(p"/\"q)"\/"q by LATTICES:def 1 .=q by XXREAL_0:36; thus maxreal.(q,minreal.(q,p))=maxreal.(q,q"/\"p) .=(p"/\"q)"\/"q by LATTICES:def 1 .=q by XXREAL_0:36; thus thesis by A1,Th2; end; theorem Th6: minreal.(q,maxreal.(q,p))=q & minreal.(maxreal.(p,q),q)=q & minreal.(q,maxreal.(p,q))=q & minreal.(maxreal.(q,p),q)=q proof set s=q"\/"p; thus A1: minreal.(q,maxreal.(q,p)) =q"/\"s .=q by XXREAL_0:35; thus A2: minreal.(maxreal.(p,q),q)=minreal.(p"\/"q,q) .=q"/\"(q"\/"p) by LATTICES:def 2 .=q by XXREAL_0:35; thus minreal.(q,maxreal.(p,q))=q by A1,Th1; thus thesis by A2,Th1; end; theorem Th7: minreal.(q,maxreal.(p,r))=maxreal.(minreal.(q,p),minreal.(q,r)) proof set s=p"\/"r; thus minreal.(q,maxreal.(p,r)) =q"/\"s .=(q"/\"p)"\/"(q"/\"r) by XXREAL_0:38 .=maxreal.(minreal.(q,p),minreal.(q,r)); end; registration cluster Real_Lattice -> distributive; coherence by Lm5; end; reserve A,B for non empty set; reserve f,g,h for Element of Funcs(A,REAL); definition let A; func maxfuncreal(A) -> BinOp of Funcs(A,REAL) means :Def4: it.(f,g) = maxreal.:(f,g); existence proof deffunc O(Element of Funcs(A,REAL),Element of Funcs(A,REAL)) = maxreal.:( \$1,\$2); ex o being BinOp of Funcs(A,REAL) st for a,b being Element of Funcs(A, REAL) holds o.(a,b) = O(a,b) from BINOP_1:sch 4; hence thesis; end; uniqueness proof let F1,F2 be BinOp of Funcs(A,REAL) such that A1: for f,g being Element of Funcs(A,REAL) holds F1.(f,g) = maxreal.:( f,g) and A2: for f,g being Element of Funcs(A,REAL) holds F2.(f,g) = maxreal.:( f,g); now let f,g be Element of Funcs(A,REAL); thus F1.(f,g) = maxreal.:(f,g) by A1 .= F2.(f,g) by A2; end; hence thesis by BINOP_1:2; end; func minfuncreal(A) -> BinOp of Funcs(A,REAL) means :Def5: it.(f,g) = minreal.:(f,g); existence proof deffunc O(Element of Funcs(A,REAL),Element of Funcs(A,REAL)) = minreal.:( \$1,\$2); ex o being BinOp of Funcs(A,REAL) st for a,b being Element of Funcs(A, REAL) holds o.(a,b) = O(a,b) from BINOP_1:sch 4; hence thesis; end; uniqueness proof let F1,F2 be BinOp of Funcs(A,REAL) such that A3: for f,g being Element of Funcs(A,REAL) holds F1.(f,g) = minreal.: (f,g) and A4: for f,g being Element of Funcs(A,REAL) holds F2.(f,g) = minreal.: (f,g); now let f,g be Element of Funcs(A,REAL); thus F1.(f,g) = minreal.:(f,g) by A3 .= F2.(f,g) by A4; end; hence thesis by BINOP_1:2; end; end; Lm6: for x being Element of A, f being Function of A,B holds x in dom f proof let x be Element of A,f be Function of A,B; x in A; hence thesis by FUNCT_2:def 1; end; theorem Th8: (maxfuncreal(A)).(f,g) = (maxfuncreal(A)).(g,f) proof now let x be Element of A; A1: x in dom (maxreal.:(f,g)) by Lm6; A2: x in dom (maxreal.:(g,f)) by Lm6; thus ((maxfuncreal(A)).(f,g)).x = (maxreal.:(f,g)).x by Def4 .= maxreal.(f.x,g.x) by A1,FUNCOP_1:22 .= maxreal.(g.x,f.x) by Th1 .= (maxreal.:(g,f)).x by A2,FUNCOP_1:22 .= ((maxfuncreal(A)).(g,f)).x by Def4; end; hence thesis by FUNCT_2:63; end; theorem Th9: (minfuncreal(A)).(f,g) = (minfuncreal(A)).(g,f) proof now let x be Element of A; A1: x in dom (minreal.:(f,g)) by Lm6; A2: x in dom (minreal.:(g,f)) by Lm6; thus ((minfuncreal(A)).(f,g)).x = (minreal.:(f,g)).x by Def5 .= minreal.(f.x,g.x) by A1,FUNCOP_1:22 .= minreal.(g.x,f.x) by Th2 .= (minreal.:(g,f)).x by A2,FUNCOP_1:22 .= ((minfuncreal(A)).(g,f)).x by Def5; end; hence thesis by FUNCT_2:63; end; theorem Th10: (maxfuncreal(A)).((maxfuncreal(A)).(f,g),h) =(maxfuncreal(A)).(f ,(maxfuncreal(A)).(g,h)) proof now let x be Element of A; A1: x in dom (maxreal.:(f,g)) by Lm6; A2: x in dom (maxreal.:(g,h)) by Lm6; A3: x in dom (maxreal.:((maxreal.:(f,g)),h)) by Lm6; A4: x in dom (maxreal.:(f,(maxreal.:(g,h)))) by Lm6; thus ((maxfuncreal(A)).((maxfuncreal(A)).(f,g),h)).x =((maxfuncreal(A)).( maxreal.:(f,g),h)).x by Def4 .=(maxreal.:(maxreal.:(f,g),h)).x by Def4 .=maxreal.((maxreal.:(f,g)).x,h.x) by A3,FUNCOP_1:22 .=maxreal.(maxreal.(f.x,g.x),h.x) by A1,FUNCOP_1:22 .=maxreal.(f.x,maxreal.(g.x,h.x)) by Th3 .=maxreal.(f.x,((maxreal.:(g,h)).x)) by A2,FUNCOP_1:22 .=(maxreal.:(f,(maxreal.:(g,h)))).x by A4,FUNCOP_1:22 .=((maxfuncreal(A)).(f,(maxreal.:(g,h)))).x by Def4 .=((maxfuncreal(A)).(f,((maxfuncreal(A)).(g,h)))).x by Def4; end; hence thesis by FUNCT_2:63; end; theorem Th11: (minfuncreal(A)).((minfuncreal(A)).(f,g),h) =(minfuncreal(A)).(f ,(minfuncreal(A)).(g,h)) proof now let x be Element of A; A1: x in dom (minreal.:(f,g)) by Lm6; A2: x in dom (minreal.:(g,h)) by Lm6; A3: x in dom (minreal.:((minreal.:(f,g)),h)) by Lm6; A4: x in dom (minreal.:(f,(minreal.:(g,h)))) by Lm6; thus ((minfuncreal(A)).((minfuncreal(A)).(f,g),h)).x =((minfuncreal(A)).( minreal.:(f,g),h)).x by Def5 .=(minreal.:(minreal.:(f,g),h)).x by Def5 .=minreal.((minreal.:(f,g)).x,h.x) by A3,FUNCOP_1:22 .=minreal.(minreal.(f.x,g.x),h.x) by A1,FUNCOP_1:22 .=minreal.(f.x,minreal.(g.x,h.x)) by Th4 .=minreal.(f.x,((minreal.:(g,h)).x)) by A2,FUNCOP_1:22 .=(minreal.:(f,(minreal.:(g,h)))).x by A4,FUNCOP_1:22 .=((minfuncreal(A)).(f,(minreal.:(g,h)))).x by Def5 .=((minfuncreal(A)).(f,((minfuncreal(A)).(g,h)))).x by Def5; end; hence thesis by FUNCT_2:63; end; theorem Th12: (maxfuncreal(A)).(f,(minfuncreal(A)).(f,g))=f proof now let x be Element of A; A1: x in dom (minreal.:(f,g)) by Lm6; A2: x in dom (maxreal.:(f,(minreal.:(f,g)))) by Lm6; thus (maxfuncreal(A)).(f,(minfuncreal(A)).(f,g)).x =((maxfuncreal(A)).(f, minreal.:(f,g))).x by Def5 .=(maxreal.:(f,minreal.:(f,g))).x by Def4 .=maxreal.(f.x,(minreal.:(f,g)).x) by A2,FUNCOP_1:22 .=maxreal.(f.x,(minreal.(f.x,g.x))) by A1,FUNCOP_1:22 .=f.x by Th5; end; hence thesis by FUNCT_2:63; end; theorem Th13: (maxfuncreal(A)).((minfuncreal(A)).(f,g),f)=f proof thus (maxfuncreal(A)).((minfuncreal(A)).(f,g),f) =(maxfuncreal(A)).(f,( minfuncreal(A)).(f,g)) by Th8 .=f by Th12; end; theorem Th14: (maxfuncreal(A)).((minfuncreal(A)).(g,f),f)=f proof thus (maxfuncreal(A)).((minfuncreal(A)).(g,f),f) =(maxfuncreal(A)).(( minfuncreal(A)).(f,g),f) by Th9 .=f by Th13; end; theorem (maxfuncreal(A)).(f,(minfuncreal(A)).(g,f))=f proof thus (maxfuncreal(A)).(f,(minfuncreal(A)).(g,f)) =(maxfuncreal(A)).(f,( minfuncreal(A)).(f,g)) by Th9 .=f by Th12; end; theorem Th16: (minfuncreal(A)).(f,(maxfuncreal(A)).(f,g))=f proof now let x be Element of A; A1: x in dom (maxreal.:(f,g)) by Lm6; A2: x in dom (minreal.:(f,(maxreal.:(f,g)))) by Lm6; thus (minfuncreal(A)).(f,(maxfuncreal(A)).(f,g)).x =((minfuncreal(A)).(f, maxreal.:(f,g))).x by Def4 .=(minreal.:(f,maxreal.:(f,g))).x by Def5 .=minreal.(f.x,(maxreal.:(f,g)).x) by A2,FUNCOP_1:22 .=minreal.(f.x,(maxreal.(f.x,g.x))) by A1,FUNCOP_1:22 .=f.x by Th6; end; hence thesis by FUNCT_2:63; end; theorem Th17: (minfuncreal(A)).(f,(maxfuncreal(A)).(g,f))=f proof thus (minfuncreal(A)).(f,(maxfuncreal(A)).(g,f)) =(minfuncreal(A)).(f,( maxfuncreal(A)).(f,g)) by Th8 .=f by Th16; end; theorem Th18: (minfuncreal(A)).((maxfuncreal(A)).(g,f),f)=f proof thus (minfuncreal(A)).((maxfuncreal(A)).(g,f),f) =(minfuncreal(A)).(f,( maxfuncreal(A)).(g,f)) by Th9 .=f by Th17; end; theorem (minfuncreal(A)).((maxfuncreal(A)).(f,g),f)=f proof thus (minfuncreal(A)).((maxfuncreal(A)).(f,g),f) =(minfuncreal(A)).(( maxfuncreal(A)).(g,f),f) by Th8 .=f by Th18; end; theorem Th20: (minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)) = (maxfuncreal(A)).( (minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h)) proof now let x be Element of A; A1: x in dom (minreal.:(f,g)) by Lm6; A2: x in dom (minreal.:(f,h)) by Lm6; A3: x in dom (minreal.:(f,(maxreal.:(g,h)))) by Lm6; A4: x in dom (maxreal.:(minreal.:(f,g),minreal.:(f,h))) by Lm6; A5: x in dom (maxreal.:(g,h)) by Lm6; thus (minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)).x =((minfuncreal(A)).(f, maxreal.:(g,h))).x by Def4 .=(minreal.:(f,maxreal.:(g,h))).x by Def5 .=minreal.(f.x,(maxreal.:(g,h)).x) by A3,FUNCOP_1:22 .=minreal.(f.x,(maxreal.(g.x,h.x))) by A5,FUNCOP_1:22 .=maxreal.(minreal.(f.x,g.x),minreal.(f.x,h.x)) by Th7 .=maxreal.(minreal.:(f,g).x,minreal.(f.x,h.x)) by A1,FUNCOP_1:22 .=maxreal.(minreal.:(f,g).x,minreal.:(f,h).x) by A2,FUNCOP_1:22 .=maxreal.:(minreal.:(f,g),minreal.:(f,h)).x by A4,FUNCOP_1:22 .=(maxfuncreal(A)).(minreal.:(f,g),minreal.:(f,h)).x by Def4 .=(maxfuncreal(A)).((minfuncreal(A)).(f,g),minreal.:(f,h)).x by Def5 .=(maxfuncreal(A)).((minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h)).x by Def5; end; hence thesis by FUNCT_2:63; end; Lm7: for a,b,c being Element of LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) holds a"\/"(b"\/"c) = (a"\/"b)"\/"c by Th10; Lm8: for a,b,c being Element of LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) holds a"/\"(b"/\"c) = (a"/\"b)"/\"c by Th11; definition let A; func RealFunc_Lattice A -> non empty strict LattStr equals LattStr (# Funcs(A,REAL), maxfuncreal A, minfuncreal A #); coherence; end; reserve L for non empty LattStr, p,q,r for Element of L; registration let A; cluster RealFunc_Lattice A -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing for non empty LattStr; coherence by Th8,Th10,Th14,Th9,Th11,Th16; end; reserve p,q,r for Element of RealFunc_Lattice(A); theorem Th21: (maxfuncreal(A)).(p,q) = (maxfuncreal(A)).(q,p) proof thus (maxfuncreal(A)).(p,q) = q"\/"p by LATTICES:def 1 .= (maxfuncreal(A)).(q,p); end; theorem Th22: (minfuncreal(A)).(p,q) = (minfuncreal(A)).(q,p) proof thus (minfuncreal(A)).(p,q) = q"/\"p by LATTICES:def 2 .= (minfuncreal(A)).(q,p); end; theorem (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) =(maxfuncreal(A)).((( maxfuncreal(A)).(q,r)),p) & (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) =( maxfuncreal(A)).(((maxfuncreal(A)).(p,q)),r) & (maxfuncreal(A)).(p,(( maxfuncreal(A)).(q,r))) =(maxfuncreal(A)).(((maxfuncreal(A)).(q,p)),r) & ( maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) =(maxfuncreal(A)).(((maxfuncreal(A )).(r,p)),q) & (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) =(maxfuncreal(A)). (((maxfuncreal(A)).(r,q)),p) & (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) =( maxfuncreal(A)).(((maxfuncreal(A)).(p,r)),q) proof set s=q"\/"r; thus A1: (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) = s"\/"p by LATTICES:def 1 .= (maxfuncreal(A)).(((maxfuncreal(A)).(q,r)),p); thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) = (maxfuncreal(A)).(( maxfuncreal(A)).(p,q),r) by Th10; thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) = p"\/"s .= (q"\/"p)"\/"r by Lm7 .= (maxfuncreal(A)).((maxfuncreal(A)).(q,p),r); thus A2: (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r))) = p"\/"(q"\/"r) .= (r"\/"p)"\/"q by Lm7 .= (maxfuncreal(A)).((maxfuncreal(A)).(r,p),q); thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))= (maxfuncreal(A)).((( maxfuncreal(A)).(r,q)),p) by A1,Th21; thus thesis by A2,Th21; end; theorem (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =(minfuncreal(A)).((( minfuncreal(A)).(q,r)),p) & (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =( minfuncreal(A)).(((minfuncreal(A)).(p,q)),r) & (minfuncreal(A)).(p,(( minfuncreal(A)).(q,r))) =(minfuncreal(A)).(((minfuncreal(A)).(q,p)),r) & ( minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =(minfuncreal(A)).(((minfuncreal(A )).(r,p)),q) & (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =(minfuncreal(A)). (((minfuncreal(A)).(r,q)),p) & (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =( minfuncreal(A)).(((minfuncreal(A)).(p,r)),q) proof set s=q"/\"r; thus A1: (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) = s"/\"p by LATTICES:def 2 .= (minfuncreal(A)).(((minfuncreal(A)).(q,r)),p); thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) = (minfuncreal(A)).(( minfuncreal(A)).(p,q),r) by Th11; thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) = p"/\"s .= (q"/\"p)"/\"r by Lm8 .= (minfuncreal(A)).((minfuncreal(A)).(q,p),r); thus A2: (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) = p"/\"(q"/\"r) .= (r"/\"p)"/\"q by Lm8 .= (minfuncreal(A)).((minfuncreal(A)).(r,p),q); thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r))) =(minfuncreal(A)).((( minfuncreal(A)).(r,q)),p) by A1,Th22; thus thesis by A2,Th22; end; theorem (maxfuncreal(A)).((minfuncreal(A)).(p,q),q)=q & (maxfuncreal(A)).(q,( minfuncreal(A)).(p,q))=q & (maxfuncreal(A)).(q,(minfuncreal(A)).(q,p))=q & ( maxfuncreal(A)).((minfuncreal(A)).(q,p),q)=q proof thus A1: (maxfuncreal(A)).((minfuncreal(A)).(p,q),q) =q by Th14; thus (maxfuncreal(A)).(q,(minfuncreal(A)).(p,q)) =(p"/\"q)"\/"q by LATTICES:def 1 .=q by Th14; thus (maxfuncreal(A)).(q,(minfuncreal(A)).(q,p)) =(maxfuncreal(A)).(q,q"/\"p ) .=(p"/\"q)"\/"q by LATTICES:def 1 .=q by Th14; thus thesis by A1,Th22; end; theorem (minfuncreal(A)).(q,(maxfuncreal(A)).(q,p))=q & (minfuncreal(A)).(( maxfuncreal(A)).(p,q),q)=q & (minfuncreal(A)).(q,(maxfuncreal(A)).(p,q))=q & ( minfuncreal(A)).((maxfuncreal(A)).(q,p),q)=q proof thus A1: (minfuncreal(A)).(q,(maxfuncreal(A)).(q,p)) =q by Th16; thus A2: (minfuncreal(A)).((maxfuncreal(A)).(p,q),q) =(minfuncreal(A)).(p "\/"q,q) .=q"/\"(q"\/"p) by LATTICES:def 2 .=q by Th16; thus (minfuncreal(A)).(q,(maxfuncreal(A)).(p,q))=q by A1,Th21; thus thesis by A2,Th21; end; theorem (minfuncreal(A)).(q,(maxfuncreal(A)).(p,r)) =(maxfuncreal(A)).(( minfuncreal(A)).(q,p),(minfuncreal(A)).(q,r)) by Th20; theorem RealFunc_Lattice(A) is D_Lattice proof p"/\"(q"\/"r) = (p"/\"q)"\/"(p"/\"r) by Th20; hence thesis by LATTICES:def 11; end;