:: The Lattice of Real Numbers. The Lattice of Real Functions
:: by Marek Chmur
::
:: Received May 22, 1990
:: Copyright (c) 1990-2026 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;
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;