:: 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;