:: REAL_LAT semantic presentation

begin


definition
func minreal  ->  BinOp of REAL means :Def1: :: REAL_LAT:def 1
 for x, y being Real holds it . (x,y) = min (x,y);
existence
 ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = min (x,y)
proof
 ex o being BinOp of REAL st
for a, b being Element of REAL holds o . (a,b) = min (a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = min (x,y) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of REAL st ( for x, y being Real holds b1 . (x,y) = min (x,y) ) & ( for x, y being Real holds b2 . (x,y) = min (x,y) ) holds
b1 = b2
proof
let f1, f2 be BinOp of REAL; ::_thesis: ( ( for x, y being Real holds f1 . (x,y) = min (x,y) ) & ( for x, y being Real holds f2 . (x,y) = min (x,y) ) implies f1 = f2 )
assume that
A1: for x, y being Real holds f1 . (x,y) = min (x,y) and
A2: for x, y being Real holds f2 . (x,y) = min (x,y) ; ::_thesis: f1 = f2
 for x, y being Element of REAL holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of REAL ; ::_thesis: f1 . (x,y) = f2 . (x,y)
 f1 . (x,y) = min (x,y) by A1;
hence  f1 . (x,y) = f2 . (x,y) by A2; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
func maxreal  ->  BinOp of REAL means :Def2: :: REAL_LAT:def 2
 for x, y being Real holds it . (x,y) = max (x,y);
existence
 ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = max (x,y)
proof
 ex o being BinOp of REAL st
for a, b being Element of REAL holds o . (a,b) = max (a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = max (x,y) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of REAL st ( for x, y being Real holds b1 . (x,y) = max (x,y) ) & ( for x, y being Real holds b2 . (x,y) = max (x,y) ) holds
b1 = b2
proof
let f1, f2 be BinOp of REAL; ::_thesis: ( ( for x, y being Real holds f1 . (x,y) = max (x,y) ) & ( for x, y being Real holds f2 . (x,y) = max (x,y) ) implies f1 = f2 )
assume that
A3: for x, y being Real holds f1 . (x,y) = max (x,y) and
A4: for x, y being Real holds f2 . (x,y) = max (x,y) ; ::_thesis: f1 = f2
 for x, y being Element of REAL holds f1 . (x,y) = f2 . (x,y)
proof
let x, y be Element of REAL ; ::_thesis: f1 . (x,y) = f2 . (x,y)
 f1 . (x,y) = max (x,y) by A3;
hence  f1 . (x,y) = f2 . (x,y) by A4; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines minreal REAL_LAT:def_1_:_
 for b1 being BinOp of REAL holds
( b1 = minreal iff for x, y being Real holds b1 . (x,y) = min (x,y) );

:: deftheorem Def2 defines maxreal REAL_LAT:def_2_:_
 for b1 being BinOp of REAL holds
( b1 = maxreal iff for x, y being Real holds b1 . (x,y) = max (x,y) );

definition
func Real_Lattice  ->  strict LattStr  equals :: REAL_LAT:def 3
 LattStr(# REAL,maxreal,minreal #);
coherence
 LattStr(# REAL,maxreal,minreal #) is strict LattStr ;
end;

:: deftheorem  defines Real_Lattice REAL_LAT:def_3_:_
 Real_Lattice = LattStr(# REAL,maxreal,minreal #);

registration
cluster the carrier of Real_Lattice ->  real-membered ;
coherence
 the carrier of Real_Lattice is real-membered ;
end;

registration
cluster Real_Lattice  ->  non empty strict ;
coherence
 not Real_Lattice is empty ;
end;


registration
let a, b be Element of Real_Lattice;
identifya "\/" b with  max (a,b);
compatibility
 a "\/" b = max (a,b) by Def2;
identifya "/\" b with  min (a,b);
compatibility
 a "/\" b = min (a,b) by Def1;
end;

Lm1:  for a, b being Element of Real_Lattice holds a "\/" b = b "\/" a
;

Lm2:  for a, b, c being Element of Real_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by XXREAL_0:34;

Lm3:  for a, b being Element of Real_Lattice holds (a "/\" b) "\/" b = b
by XXREAL_0:36;

Lm4:  for a, b being Element of Real_Lattice holds a "/\" b = b "/\" a
;

Lm5:  for a, b, c being Element of Real_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by XXREAL_0:33;

Lm6:  for a, b being Element of Real_Lattice holds a "/\" (a "\/" b) = a
by XXREAL_0:35;

registration
cluster Real_Lattice  ->  strict Lattice-like ;
coherence
 Real_Lattice is Lattice-like
proof
 ( Real_Lattice is join-commutative & Real_Lattice is join-associative & Real_Lattice is meet-absorbing & Real_Lattice is meet-commutative & Real_Lattice is meet-associative & Real_Lattice is join-absorbing ) by Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  Real_Lattice is Lattice-like ; ::_thesis: verum
end;
end;

Lm7:  for a, b, c being Element of Real_Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
by XXREAL_0:38;


theorem Th1: :: REAL_LAT:1
for p, q being Element of Real_Lattice holds maxreal . (p,q) = maxreal . (q,p)
proof
let p, q be Element of Real_Lattice; ::_thesis: maxreal . (p,q) = maxreal . (q,p)
thus maxreal . (p,q) = q "\/" p by LATTICES:def_1
.= maxreal . (q,p) ; ::_thesis: verum
end;

theorem Th2: :: REAL_LAT:2
for p, q being Element of Real_Lattice holds minreal . (p,q) = minreal . (q,p)
proof
let p, q be Element of Real_Lattice; ::_thesis: minreal . (p,q) = minreal . (q,p)
thus minreal . (p,q) = q "/\" p by LATTICES:def_2
.= minreal . (q,p) ; ::_thesis: verum
end;

theorem Th3: :: REAL_LAT:3
for p, q, r being Element of Real_Lattice holds
( 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
let p, q, r be Element of Real_Lattice; ::_thesis: ( 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) )
set s = q "\/" r;
thus A1: maxreal . (p,(maxreal . (q,r))) = (q "\/" r) "\/" p by LATTICES:def_1
.= maxreal . ((maxreal . (q,r)),p) ; ::_thesis: ( 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) )
thus maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (p "\/" q) "\/" r by XXREAL_0:34
.= maxreal . ((maxreal . (p,q)),r) ; ::_thesis: ( 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) )
thus maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (q "\/" p) "\/" r by XXREAL_0:34
.= maxreal . ((maxreal . (q,p)),r) ; ::_thesis: ( 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) )
thus A2: maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (r "\/" p) "\/" q by XXREAL_0:34
.= maxreal . ((maxreal . (r,p)),q) ; ::_thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
thus  maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) by A1, Th1; ::_thesis: maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q)
thus  maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) by A2, Th1; ::_thesis: verum
end;

theorem Th4: :: REAL_LAT:4
for p, q, r being Element of Real_Lattice holds
( 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
let p, q, r be Element of Real_Lattice; ::_thesis: ( 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) )
set s = q "/\" r;
thus A1: minreal . (p,(minreal . (q,r))) = (q "/\" r) "/\" p by LATTICES:def_2
.= minreal . ((minreal . (q,r)),p) ; ::_thesis: ( 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) )
thus minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (p "/\" q) "/\" r by XXREAL_0:33
.= minreal . ((minreal . (p,q)),r) ; ::_thesis: ( 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) )
thus minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (q "/\" p) "/\" r by XXREAL_0:33
.= minreal . ((minreal . (q,p)),r) ; ::_thesis: ( 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) )
thus A2: minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (r "/\" p) "/\" q by XXREAL_0:33
.= minreal . ((minreal . (r,p)),q) ; ::_thesis: ( minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,q)),p) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q) )
thus  minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,q)),p) by A1, Th2; ::_thesis: minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q)
thus  minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q) by A2, Th2; ::_thesis: verum
end;

theorem Th5: :: REAL_LAT:5
for p, q being Element of Real_Lattice holds
( 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
let p, q be Element of Real_Lattice; ::_thesis: ( maxreal . ((minreal . (p,q)),q) = q & maxreal . (q,(minreal . (p,q))) = q & maxreal . (q,(minreal . (q,p))) = q & maxreal . ((minreal . (q,p)),q) = q )
set s = p "/\" q;
thus A1: maxreal . ((minreal . (p,q)),q) = (p "/\" q) "\/" q
.= q by XXREAL_0:36 ; ::_thesis: ( maxreal . (q,(minreal . (p,q))) = q & maxreal . (q,(minreal . (q,p))) = q & maxreal . ((minreal . (q,p)),q) = q )
thus maxreal . (q,(minreal . (p,q))) = (p "/\" q) "\/" q by LATTICES:def_1
.= q by XXREAL_0:36 ; ::_thesis: ( maxreal . (q,(minreal . (q,p))) = q & maxreal . ((minreal . (q,p)),q) = q )
thus maxreal . (q,(minreal . (q,p))) = maxreal . (q,(q "/\" p))
.= (p "/\" q) "\/" q by LATTICES:def_1
.= q by XXREAL_0:36 ; ::_thesis: maxreal . ((minreal . (q,p)),q) = q
thus  maxreal . ((minreal . (q,p)),q) = q by A1, Th2; ::_thesis: verum
end;

theorem Th6: :: REAL_LAT:6
for q, p being Element of Real_Lattice holds
( 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
let q, p be Element of Real_Lattice; ::_thesis: ( minreal . (q,(maxreal . (q,p))) = q & minreal . ((maxreal . (p,q)),q) = q & minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
set s = q "\/" p;
thus A1: minreal . (q,(maxreal . (q,p))) = q "/\" (q "\/" p)
.= q by XXREAL_0:35 ; ::_thesis: ( minreal . ((maxreal . (p,q)),q) = q & minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
thus A2: minreal . ((maxreal . (p,q)),q) = minreal . ((p "\/" q),q)
.= q "/\" (q "\/" p) by LATTICES:def_2
.= q by XXREAL_0:35 ; ::_thesis: ( minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
thus  minreal . (q,(maxreal . (p,q))) = q by A1, Th1; ::_thesis: minreal . ((maxreal . (q,p)),q) = q
thus  minreal . ((maxreal . (q,p)),q) = q by A2, Th1; ::_thesis: verum
end;

theorem Th7: :: REAL_LAT:7
for q, p, r being Element of Real_Lattice holds minreal . (q,(maxreal . (p,r))) = maxreal . ((minreal . (q,p)),(minreal . (q,r)))
proof
let q, p, r be Element of Real_Lattice; ::_thesis: minreal . (q,(maxreal . (p,r))) = maxreal . ((minreal . (q,p)),(minreal . (q,r)))
set s = p "\/" r;
thus minreal . (q,(maxreal . (p,r))) = q "/\" (p "\/" r)
.= (q "/\" p) "\/" (q "/\" r) by XXREAL_0:38
.= maxreal . ((minreal . (q,p)),(minreal . (q,r))) ; ::_thesis: verum
end;

registration
cluster Real_Lattice  ->  strict distributive ;
coherence
 Real_Lattice is distributive by Lm7, LATTICES:def_11;
end;


definition
let A be non empty set ;
func maxfuncreal A ->  BinOp of (Funcs (A,REAL)) means :Def4: :: REAL_LAT:def 4
 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = maxreal .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = maxreal .: (f,g)
proof
deffunc H1( Element of Funcs (A,REAL), 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) = H1(a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = maxreal .: (f,g) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = maxreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = maxreal .: (f,g) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = maxreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = maxreal .: (f,g) ) implies F1 = F2 )
assume 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) ; ::_thesis: F1 = F2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_F1_._(f,g)_=_F2_._(f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: F1 . (f,g) = F2 . (f,g)
thus F1 . (f,g) = maxreal .: (f,g) by A1
.= F2 . (f,g) by A2 ; ::_thesis: verum
end;
hence  F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
func minfuncreal A ->  BinOp of (Funcs (A,REAL)) means :Def5: :: REAL_LAT:def 5
 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = minreal .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = minreal .: (f,g)
proof
deffunc H1( Element of Funcs (A,REAL), 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) = H1(a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = minreal .: (f,g) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = minreal .: (f,g) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = minreal .: (f,g) ) implies F1 = F2 )
assume 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) ; ::_thesis: F1 = F2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_F1_._(f,g)_=_F2_._(f,g)
let f, g be Element of Funcs (A,REAL); ::_thesis: F1 . (f,g) = F2 . (f,g)
thus F1 . (f,g) = minreal .: (f,g) by A3
.= F2 . (f,g) by A4 ; ::_thesis: verum
end;
hence  F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines maxfuncreal REAL_LAT:def_4_:_
 for A being non empty set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = maxfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = maxreal .: (f,g) );

:: deftheorem Def5 defines minfuncreal REAL_LAT:def_5_:_
 for A being non empty set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = minfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = minreal .: (f,g) );

Lm8:  for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proof
let A, B be non empty set ; ::_thesis: for x being Element of A
for f being Function of A,B holds x in dom f
let x be Element of A; ::_thesis: for f being Function of A,B holds x in dom f
let f be Function of A,B; ::_thesis: x in dom f
 x in A ;
hence  x in dom f by FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th8: :: REAL_LAT:8
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
let f, g be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)
now__::_thesis:_for_x_being_Element_of_A_holds_((maxfuncreal_A)_._(f,g))_._x_=_((maxfuncreal_A)_._(g,f))_._x
let x be Element of A; ::_thesis: ((maxfuncreal A) . (f,g)) . x = ((maxfuncreal A) . (g,f)) . x
A1: x in dom (maxreal .: (f,g)) by Lm8;
A2: x in dom (maxreal .: (g,f)) by Lm8;
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 ; ::_thesis: verum
end;
hence  (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th9: :: REAL_LAT:9
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,g) = (minfuncreal A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,g) = (minfuncreal A) . (g,f)
let f, g be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (f,g) = (minfuncreal A) . (g,f)
now__::_thesis:_for_x_being_Element_of_A_holds_((minfuncreal_A)_._(f,g))_._x_=_((minfuncreal_A)_._(g,f))_._x
let x be Element of A; ::_thesis: ((minfuncreal A) . (f,g)) . x = ((minfuncreal A) . (g,f)) . x
A1: x in dom (minreal .: (f,g)) by Lm8;
A2: x in dom (minreal .: (g,f)) by Lm8;
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 ; ::_thesis: verum
end;
hence  (minfuncreal A) . (f,g) = (minfuncreal A) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th10: :: REAL_LAT:10
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (g,h)))
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (g,h)))
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (g,h)))
now__::_thesis:_for_x_being_Element_of_A_holds_((maxfuncreal_A)_._(((maxfuncreal_A)_._(f,g)),h))_._x_=_((maxfuncreal_A)_._(f,((maxfuncreal_A)_._(g,h))))_._x
let x be Element of A; ::_thesis: ((maxfuncreal A) . (((maxfuncreal A) . (f,g)),h)) . x = ((maxfuncreal A) . (f,((maxfuncreal A) . (g,h)))) . x
A1: x in dom (maxreal .: (f,g)) by Lm8;
A2: x in dom (maxreal .: (g,h)) by Lm8;
A3: x in dom (maxreal .: ((maxreal .: (f,g)),h)) by Lm8;
A4: x in dom (maxreal .: (f,(maxreal .: (g,h)))) by Lm8;
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 ; ::_thesis: verum
end;
hence  (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (g,h))) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th11: :: REAL_LAT:11
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))
now__::_thesis:_for_x_being_Element_of_A_holds_((minfuncreal_A)_._(((minfuncreal_A)_._(f,g)),h))_._x_=_((minfuncreal_A)_._(f,((minfuncreal_A)_._(g,h))))_._x
let x be Element of A; ::_thesis: ((minfuncreal A) . (((minfuncreal A) . (f,g)),h)) . x = ((minfuncreal A) . (f,((minfuncreal A) . (g,h)))) . x
A1: x in dom (minreal .: (f,g)) by Lm8;
A2: x in dom (minreal .: (g,h)) by Lm8;
A3: x in dom (minreal .: ((minreal .: (f,g)),h)) by Lm8;
A4: x in dom (minreal .: (f,(minreal .: (g,h)))) by Lm8;
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 ; ::_thesis: verum
end;
hence  (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h))) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th12: :: REAL_LAT:12
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) = f
now__::_thesis:_for_x_being_Element_of_A_holds_((maxfuncreal_A)_._(f,((minfuncreal_A)_._(f,g))))_._x_=_f_._x
let x be Element of A; ::_thesis: ((maxfuncreal A) . (f,((minfuncreal A) . (f,g)))) . x = f . x
A1: x in dom (minreal .: (f,g)) by Lm8;
A2: x in dom (maxreal .: (f,(minreal .: (f,g)))) by Lm8;
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 ; ::_thesis: verum
end;
hence  (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th13: :: REAL_LAT:13
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) = f
thus (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) = (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) by Th8
.= f by Th12 ; ::_thesis: verum
end;

theorem Th14: :: REAL_LAT:14
for A being non empty set
for g, f being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (g,f)),f) = f
proof
let A be non empty set ; ::_thesis: for g, f being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (g,f)),f) = f
let g, f be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (((minfuncreal A) . (g,f)),f) = f
thus (maxfuncreal A) . (((minfuncreal A) . (g,f)),f) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) by Th9
.= f by Th13 ; ::_thesis: verum
end;

theorem :: REAL_LAT:15
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (g,f))) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (g,f))) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (maxfuncreal A) . (f,((minfuncreal A) . (g,f))) = f
thus (maxfuncreal A) . (f,((minfuncreal A) . (g,f))) = (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) by Th9
.= f by Th12 ; ::_thesis: verum
end;

theorem Th16: :: REAL_LAT:16
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) = f
now__::_thesis:_for_x_being_Element_of_A_holds_((minfuncreal_A)_._(f,((maxfuncreal_A)_._(f,g))))_._x_=_f_._x
let x be Element of A; ::_thesis: ((minfuncreal A) . (f,((maxfuncreal A) . (f,g)))) . x = f . x
A1: x in dom (maxreal .: (f,g)) by Lm8;
A2: x in dom (minreal .: (f,(maxreal .: (f,g)))) by Lm8;
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 ; ::_thesis: verum
end;
hence  (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th17: :: REAL_LAT:17
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) = f
thus (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) = (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) by Th8
.= f by Th16 ; ::_thesis: verum
end;

theorem Th18: :: REAL_LAT:18
for A being non empty set
for g, f being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) = f
proof
let A be non empty set ; ::_thesis: for g, f being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) = f
let g, f be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) = f
thus (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) = (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) by Th9
.= f by Th17 ; ::_thesis: verum
end;

theorem :: REAL_LAT:19
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (f,g)),f) = f
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (f,g)),f) = f
let f, g be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (((maxfuncreal A) . (f,g)),f) = f
thus (minfuncreal A) . (((maxfuncreal A) . (f,g)),f) = (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) by Th8
.= f by Th18 ; ::_thesis: verum
end;

theorem Th20: :: REAL_LAT:20
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))
let f, g, h be Element of Funcs (A,REAL); ::_thesis: (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))
now__::_thesis:_for_x_being_Element_of_A_holds_((minfuncreal_A)_._(f,((maxfuncreal_A)_._(g,h))))_._x_=_((maxfuncreal_A)_._(((minfuncreal_A)_._(f,g)),((minfuncreal_A)_._(f,h))))_._x
let x be Element of A; ::_thesis: ((minfuncreal A) . (f,((maxfuncreal A) . (g,h)))) . x = ((maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))) . x
A1: x in dom (minreal .: (f,g)) by Lm8;
A2: x in dom (minreal .: (f,h)) by Lm8;
A3: x in dom (minreal .: (f,(maxreal .: (g,h)))) by Lm8;
A4: x in dom (maxreal .: ((minreal .: (f,g)),(minreal .: (f,h)))) by Lm8;
A5: x in dom (maxreal .: (g,h)) by Lm8;
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 ; ::_thesis: verum
end;
hence  (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h))) by FUNCT_2:63; ::_thesis: verum
end;

Lm9:  for A being non empty set
for a, b, c being Element of LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by Th10;

Lm10:  for A being non empty set
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 be non empty set ;
func RealFunc_Lattice A ->  non empty strict LattStr  equals :: REAL_LAT:def 6
 LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);
coherence
 LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #) is non empty strict LattStr ;
end;

:: deftheorem  defines RealFunc_Lattice REAL_LAT:def_6_:_
 for A being non empty set holds RealFunc_Lattice A = LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);


registration
let A be non empty set ;
cluster RealFunc_Lattice A ->  non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing for non empty LattStr ;
coherence
 for b1 being non empty LattStr st b1 = RealFunc_Lattice A holds
( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing )
proof
let L be non empty LattStr ; ::_thesis: ( L = RealFunc_Lattice A implies ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) )
assume A1: L = RealFunc_Lattice A ; ::_thesis: ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for p, q being Element of L holds p "\/" q = q "\/" p by Th8, A1; :: according to LATTICES:def_4 ::_thesis: ( L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for p, q, r being Element of L holds p "\/" (q "\/" r) = (p "\/" q) "\/" r by Th10, A1; :: according to LATTICES:def_5 ::_thesis: ( L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for p, q being Element of L holds (p "/\" q) "\/" q = q by Th14, A1; :: according to LATTICES:def_8 ::_thesis: ( L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for p, q being Element of L holds p "/\" q = q "/\" p by Th9, A1; :: according to LATTICES:def_6 ::_thesis: ( L is meet-associative & L is join-absorbing )
thus  for p, q, r being Element of L holds p "/\" (q "/\" r) = (p "/\" q) "/\" r by Th11, A1; :: according to LATTICES:def_7 ::_thesis: L is join-absorbing
thus  for p, q being Element of L holds p "/\" (p "\/" q) = p by Th16, A1; :: according to LATTICES:def_9 ::_thesis: verum
end;
end;


theorem Th21: :: REAL_LAT:21
for A being non empty set
for p, q being Element of (RealFunc_Lattice A) holds (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)
proof
let A be non empty set ; ::_thesis: for p, q being Element of (RealFunc_Lattice A) holds (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)
let p, q be Element of (RealFunc_Lattice A); ::_thesis: (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)
thus (maxfuncreal A) . (p,q) = q "\/" p by LATTICES:def_1
.= (maxfuncreal A) . (q,p) ; ::_thesis: verum
end;

theorem Th22: :: REAL_LAT:22
for A being non empty set
for p, q being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (p,q) = (minfuncreal A) . (q,p)
proof
let A be non empty set ; ::_thesis: for p, q being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (p,q) = (minfuncreal A) . (q,p)
let p, q be Element of (RealFunc_Lattice A); ::_thesis: (minfuncreal A) . (p,q) = (minfuncreal A) . (q,p)
thus (minfuncreal A) . (p,q) = q "/\" p by LATTICES:def_2
.= (minfuncreal A) . (q,p) ; ::_thesis: verum
end;

theorem :: REAL_LAT:23
for A being non empty set
for p, q, r being Element of (RealFunc_Lattice A) holds
( (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
let A be non empty set ; ::_thesis: for p, q, r being Element of (RealFunc_Lattice A) holds
( (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) )
let p, q, r be Element of (RealFunc_Lattice A); ::_thesis: ( (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) )
set s = q "\/" r;
thus A1: (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = (q "\/" r) "\/" p by LATTICES:def_1
.= (maxfuncreal A) . (((maxfuncreal A) . (q,r)),p) ; ::_thesis: ( (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) )
thus  (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = (maxfuncreal A) . (((maxfuncreal A) . (p,q)),r) by Th10; ::_thesis: ( (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) )
thus (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = p "\/" (q "\/" r)
.= (q "\/" p) "\/" r by Lm9
.= (maxfuncreal A) . (((maxfuncreal A) . (q,p)),r) ; ::_thesis: ( (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) )
thus A2: (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = p "\/" (q "\/" r)
.= (r "\/" p) "\/" q by Lm9
.= (maxfuncreal A) . (((maxfuncreal A) . (r,p)),q) ; ::_thesis: ( (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) )
thus  (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = (maxfuncreal A) . (((maxfuncreal A) . (r,q)),p) by A1, Th21; ::_thesis: (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = (maxfuncreal A) . (((maxfuncreal A) . (p,r)),q)
thus  (maxfuncreal A) . (p,((maxfuncreal A) . (q,r))) = (maxfuncreal A) . (((maxfuncreal A) . (p,r)),q) by A2, Th21; ::_thesis: verum
end;

theorem :: REAL_LAT:24
for A being non empty set
for p, q, r being Element of (RealFunc_Lattice A) holds
( (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
let A be non empty set ; ::_thesis: for p, q, r being Element of (RealFunc_Lattice A) holds
( (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) )
let p, q, r be Element of (RealFunc_Lattice A); ::_thesis: ( (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) )
set s = q "/\" r;
thus A1: (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = (q "/\" r) "/\" p by LATTICES:def_2
.= (minfuncreal A) . (((minfuncreal A) . (q,r)),p) ; ::_thesis: ( (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) )
thus  (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = (minfuncreal A) . (((minfuncreal A) . (p,q)),r) by Th11; ::_thesis: ( (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) )
thus (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = p "/\" (q "/\" r)
.= (q "/\" p) "/\" r by Lm10
.= (minfuncreal A) . (((minfuncreal A) . (q,p)),r) ; ::_thesis: ( (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) )
thus A2: (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = p "/\" (q "/\" r)
.= (r "/\" p) "/\" q by Lm10
.= (minfuncreal A) . (((minfuncreal A) . (r,p)),q) ; ::_thesis: ( (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) )
thus  (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = (minfuncreal A) . (((minfuncreal A) . (r,q)),p) by A1, Th22; ::_thesis: (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = (minfuncreal A) . (((minfuncreal A) . (p,r)),q)
thus  (minfuncreal A) . (p,((minfuncreal A) . (q,r))) = (minfuncreal A) . (((minfuncreal A) . (p,r)),q) by A2, Th22; ::_thesis: verum
end;

theorem :: REAL_LAT:25
for A being non empty set
for p, q being Element of (RealFunc_Lattice A) holds
( (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
let A be non empty set ; ::_thesis: for p, q being Element of (RealFunc_Lattice A) holds
( (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 )
let p, q be Element of (RealFunc_Lattice A); ::_thesis: ( (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 )
thus A1: (maxfuncreal A) . (((minfuncreal A) . (p,q)),q) = q by Th14; ::_thesis: ( (maxfuncreal A) . (q,((minfuncreal A) . (p,q))) = q & (maxfuncreal A) . (q,((minfuncreal A) . (q,p))) = q & (maxfuncreal A) . (((minfuncreal A) . (q,p)),q) = q )
thus (maxfuncreal A) . (q,((minfuncreal A) . (p,q))) = (p "/\" q) "\/" q by LATTICES:def_1
.= q by Th14 ; ::_thesis: ( (maxfuncreal A) . (q,((minfuncreal A) . (q,p))) = q & (maxfuncreal A) . (((minfuncreal A) . (q,p)),q) = q )
thus (maxfuncreal A) . (q,((minfuncreal A) . (q,p))) = (maxfuncreal A) . (q,(q "/\" p))
.= (p "/\" q) "\/" q by LATTICES:def_1
.= q by Th14 ; ::_thesis: (maxfuncreal A) . (((minfuncreal A) . (q,p)),q) = q
thus  (maxfuncreal A) . (((minfuncreal A) . (q,p)),q) = q by A1, Th22; ::_thesis: verum
end;

theorem :: REAL_LAT:26
for A being non empty set
for q, p being Element of (RealFunc_Lattice A) holds
( (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
let A be non empty set ; ::_thesis: for q, p being Element of (RealFunc_Lattice A) holds
( (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 )
let q, p be Element of (RealFunc_Lattice A); ::_thesis: ( (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 )
thus A1: (minfuncreal A) . (q,((maxfuncreal A) . (q,p))) = q by Th16; ::_thesis: ( (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = q & (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
thus A2: (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = (minfuncreal A) . ((p "\/" q),q)
.= q "/\" (q "\/" p) by LATTICES:def_2
.= q by Th16 ; ::_thesis: ( (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
thus  (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q by A1, Th21; ::_thesis: (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q
thus  (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q by A2, Th21; ::_thesis: verum
end;

theorem :: REAL_LAT:27
for A being non empty set
for q, p, r being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (q,((maxfuncreal A) . (p,r))) = (maxfuncreal A) . (((minfuncreal A) . (q,p)),((minfuncreal A) . (q,r))) by Th20;

theorem :: REAL_LAT:28
for A being non empty set holds RealFunc_Lattice A is D_Lattice
proof
let A be non empty set ; ::_thesis: RealFunc_Lattice A is D_Lattice
 for p, q, r being Element of (RealFunc_Lattice A) holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) by Th20;
hence  RealFunc_Lattice A is D_Lattice by LATTICES:def_11; ::_thesis: verum
end;