set B = {0,1} \/ ].(1 / 2),1.[;
set L = RealSubLatt ((In (0,REAL)),(In (1,REAL)));
set R = Real_Lattice ;
A1: {0,1} \/ ].(1 / 2),1.[ c= \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) }
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {0,1} \/ ].(1 / 2),1.[ or x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } )
assume A2: x1 in {0,1} \/ ].(1 / 2),1.[ ; :: thesis: x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) }
now :: thesis: x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) }
per cases ( x1 in {0,1} or x1 in ].(1 / 2),1.[ ) by ;
suppose x1 in {0,1} ; :: thesis: x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) }
then ( x1 = 0 or x1 = 1 ) by TARSKI:def 2;
then ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= jj ) } ) by TARSKI:def 1;
hence x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x1 in ].(1 / 2),1.[ ; :: thesis: x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) }
then x1 in { r where r is Real : ( 1 / 2 < r & r < 1 ) } by RCOMP_1:def 2;
then consider y being Real such that
A3: x1 = y and
A4: ( 1 / 2 < y & y < 1 ) ;
y in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by A4;
hence x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by ; :: thesis: verum
end;
end;
end;
hence x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: verum
end;
{0} \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } c= {0,1} \/ ].(1 / 2),1.[
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } or x1 in {0,1} \/ ].(1 / 2),1.[ )
assume A5: x1 in \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: x1 in {0,1} \/ ].(1 / 2),1.[
now :: thesis: x1 in {0,1} \/ ].(1 / 2),1.[
per cases ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: x1 in {0,1} \/ ].(1 / 2),1.[
then consider y being Real such that
A6: x1 = y and
A7: 1 / 2 < y and
A8: y <= 1 ;
( y < 1 or y = 1 ) by ;
then ( y in { r where r is Real : ( 1 / 2 < r & r < 1 ) } or y = 1 ) by A7;
then ( y in ].(1 / 2),1.[ or y in {0,1} ) by ;
hence x1 in {0,1} \/ ].(1 / 2),1.[ by ; :: thesis: verum
end;
end;
end;
hence x1 in {0,1} \/ ].(1 / 2),1.[ ; :: thesis: verum
end;
then A9: {0,1} \/ ].(1 / 2),1.[ = \/ { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by ;
A10: 0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider A = [.0,jj.] as non empty set by RCOMP_1:def 1;
A11: the L_meet of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = minreal || [.0,jj.] by Def4;
reconsider B = {0,1} \/ ].(1 / 2),1.[ as non empty set ;
A12: the L_join of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = maxreal || [.0,jj.] by Def4;
A13: A = the carrier of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) by Def4;
then reconsider Ma = maxreal || A, Mi = minreal || A as BinOp of A by Def4;
A14: now :: thesis: for x1 being object st x1 in B holds
x1 in A
let x1 be object ; :: thesis: ( x1 in B implies x1 in A )
assume A15: x1 in B ; :: thesis: x1 in A
now :: thesis: x1 in A
per cases ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: x1 in A
then ex y being Real st
( x1 = y & 1 / 2 < y & y <= 1 ) ;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence x1 in A by RCOMP_1:def 1; :: thesis: verum
end;
end;
end;
hence x1 in A ; :: thesis: verum
end;
then A16: B c= A ;
then A17: [:B,B:] c= [:A,A:] by ZFMISC_1:96;
then reconsider ma = Ma || B, mi = Mi || B as Function of [:B,B:],A by FUNCT_2:32;
A18: for x1 being Element of A holds x1 is Element of Real_Lattice by ;
A19: dom mi = [:B,B:] by FUNCT_2:def 1;
A20: now :: thesis: for x9 being object st x9 in dom mi holds
mi . x9 in B
let x9 be object ; :: thesis: ( x9 in dom mi implies mi . x9 in B )
assume A21: x9 in dom mi ; :: thesis: mi . x9 in B
then consider x1, x2 being object such that
A22: x9 = [x1,x2] by RELAT_1:def 1;
A23: x2 in B by ;
A24: x1 in B by ;
now :: thesis: mi . x9 in B
per cases ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x1 in ; :: thesis: mi . x9 in B
then A25: x1 = 0 by TARSKI:def 1;
now :: thesis: mi . x9 in B
per cases ( x2 in or x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x2 in ; :: thesis: mi . x9 in B
then A26: x2 = 0 by TARSKI:def 1;
mi . x9 = Mi . [x1,x2] by
.= minreal . (x1,x2) by
.= min (0,0) by
.= 0 ;
then mi . x9 in by TARSKI:def 1;
hence mi . x9 in B by ; :: thesis: verum
end;
suppose x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: mi . x9 in B
then consider y2 being Real such that
A27: x2 = y2 and
A28: ( 1 / 2 < y2 & y2 <= 1 ) ;
reconsider y2 = y2 as Real ;
mi . x9 = Mi . [x1,x2] by
.= minreal . (x1,x2) by
.= min (0,y2) by ;
then ( mi . x9 = 0 or mi . x9 = y2 ) by XXREAL_0:15;
then ( mi . x9 in or mi . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
hence mi . x9 in B by ; :: thesis: verum
end;
end;
end;
hence mi . x9 in B ; :: thesis: verum
end;
suppose x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: mi . x9 in B
then consider y1 being Real such that
A29: x1 = y1 and
A30: ( 1 / 2 < y1 & y1 <= 1 ) ;
reconsider y1 = y1 as Real ;
now :: thesis: mi . x9 in B
per cases ( x2 in or x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x2 in ; :: thesis: mi . x9 in B
then A31: x2 = 0 by TARSKI:def 1;
mi . x9 = Mi . [x1,x2] by
.= minreal . (x1,x2) by
.= min (y1,0) by ;
then ( mi . x9 = y1 or mi . x9 = 0 ) by XXREAL_0:15;
then ( mi . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } or mi . x9 in ) by ;
hence mi . x9 in B by ; :: thesis: verum
end;
suppose x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: mi . x9 in B
then consider y2 being Real such that
A32: x2 = y2 and
A33: ( 1 / 2 < y2 & y2 <= 1 ) ;
reconsider y2 = y2 as Real ;
mi . x9 = Mi . [x1,x2] by
.= minreal . (x1,x2) by
.= min (y1,y2) by ;
then ( mi . x9 = y1 or mi . x9 = y2 ) by XXREAL_0:15;
then mi . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by ;
hence mi . x9 in B by ; :: thesis: verum
end;
end;
end;
hence mi . x9 in B ; :: thesis: verum
end;
end;
end;
hence mi . x9 in B ; :: thesis: verum
end;
A34: dom ma = [:B,B:] by FUNCT_2:def 1;
A35: now :: thesis: for x9 being object st x9 in dom ma holds
ma . x9 in B
let x9 be object ; :: thesis: ( x9 in dom ma implies ma . x9 in B )
assume A36: x9 in dom ma ; :: thesis: ma . x9 in B
then consider x1, x2 being object such that
A37: x9 = [x1,x2] by RELAT_1:def 1;
A38: x2 in B by ;
A39: x1 in B by ;
now :: thesis: ma . x9 in B
per cases ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x1 in ; :: thesis: ma . x9 in B
then A40: x1 = 0 by TARSKI:def 1;
now :: thesis: ma . x9 in B
per cases ( x2 in or x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x2 in ; :: thesis: ma . x9 in B
then A41: x2 = 0 by TARSKI:def 1;
ma . x9 = Ma . [x1,x2] by
.= maxreal . (x1,x2) by
.= max (0,0) by
.= 0 ;
then ma . x9 in by TARSKI:def 1;
hence ma . x9 in B by ; :: thesis: verum
end;
suppose x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: ma . x9 in B
then consider y2 being Real such that
A42: x2 = y2 and
A43: ( 1 / 2 < y2 & y2 <= 1 ) ;
reconsider y2 = y2 as Real ;
ma . x9 = Ma . [x1,x2] by
.= maxreal . (x1,x2) by
.= max (0,y2) by ;
then ( ma . x9 = 0 or ma . x9 = y2 ) by XXREAL_0:16;
then ( ma . x9 in or ma . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
hence ma . x9 in B by ; :: thesis: verum
end;
end;
end;
hence ma . x9 in B ; :: thesis: verum
end;
suppose x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: ma . x9 in B
then consider y1 being Real such that
A44: x1 = y1 and
A45: ( 1 / 2 < y1 & y1 <= 1 ) ;
reconsider y1 = y1 as Real ;
now :: thesis: ma . x9 in B
per cases ( x2 in or x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x2 in ; :: thesis: ma . x9 in B
then A46: x2 = 0 by TARSKI:def 1;
ma . x9 = Ma . [x1,x2] by
.= maxreal . (x1,x2) by
.= max (y1,0) by ;
then ( ma . x9 = y1 or ma . x9 = 0 ) by XXREAL_0:16;
then ( ma . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } or ma . x9 in ) by ;
hence ma . x9 in B by ; :: thesis: verum
end;
suppose x2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: ma . x9 in B
then consider y2 being Real such that
A47: x2 = y2 and
A48: ( 1 / 2 < y2 & y2 <= 1 ) ;
reconsider y2 = y2 as Real ;
ma . x9 = Ma . [x1,x2] by
.= maxreal . (x1,x2) by
.= max (y1,y2) by ;
then ( ma . x9 = y1 or ma . x9 = y2 ) by XXREAL_0:16;
then ma . x9 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by ;
hence ma . x9 in B by ; :: thesis: verum
end;
end;
end;
hence ma . x9 in B ; :: thesis: verum
end;
end;
end;
hence ma . x9 in B ; :: thesis: verum
end;
reconsider mi = mi as BinOp of B by ;
reconsider ma = ma as BinOp of B by ;
reconsider L9 = LattStr(# B,ma,mi #) as non empty LattStr ;
A49: now :: thesis: for a, b being Element of L9 holds
( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
let a, b be Element of L9; :: thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
thus a "\/" b = the L_join of L9 . (a,b) by LATTICES:def 1
.= () . [a,b] by FUNCT_1:49
.= maxreal . (a,b) by ; :: thesis: a "/\" b = minreal . (a,b)
thus a "/\" b = the L_meet of L9 . (a,b) by LATTICES:def 2
.= () . [a,b] by FUNCT_1:49
.= minreal . (a,b) by ; :: thesis: verum
end;
reconsider L = RealSubLatt ((In (0,REAL)),(In (1,REAL))) as complete Lattice by Th20;
A50: now :: thesis: for x1 being Element of B holds x1 is Element of L
let x1 be Element of B; :: thesis: x1 is Element of L
now :: thesis: x1 is Element of L
per cases ( x1 in or x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by ;
suppose x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ; :: thesis: x1 is Element of L
then ex y being Real st
( x1 = y & 1 / 2 < y & y <= 1 ) ;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence x1 is Element of L by ; :: thesis: verum
end;
end;
end;
hence x1 is Element of L ; :: thesis: verum
end;
A51: now :: thesis: for p, q being Element of L9 holds p "\/" q = q "\/" p
let p, q be Element of L9; :: thesis: p "\/" q = q "\/" p
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by ;
thus p "\/" q = maxreal . (p,q) by A49
.= maxreal . (q9,p9) by REAL_LAT:1
.= q "\/" p by A49 ; :: thesis: verum
end;
A52: now :: thesis: for p, q being Element of L9 holds p "/\" (p "\/" q) = p
let p, q be Element of L9; :: thesis: p "/\" (p "\/" q) = p
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by ;
thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A49
.= minreal . (p9,(maxreal . (p9,q9))) by A49
.= p by REAL_LAT:6 ; :: thesis: verum
end;
A53: now :: thesis: for p, q being Element of L9 holds p "/\" q = q "/\" p
let p, q be Element of L9; :: thesis: p "/\" q = q "/\" p
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by ;
thus p "/\" q = minreal . (p,q) by A49
.= minreal . (q9,p9) by REAL_LAT:2
.= q "/\" p by A49 ; :: thesis: verum
end;
A54: now :: thesis: for p, q being Element of L9 holds (p "/\" q) "\/" q = q
let p, q be Element of L9; :: thesis: (p "/\" q) "\/" q = q
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by ;
thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A49
.= maxreal . ((minreal . (p9,q9)),q9) by A49
.= q by REAL_LAT:5 ; :: thesis: verum
end;
A55: now :: thesis: for p, q, r being Element of L9 holds p "/\" (q "/\" r) = (p "/\" q) "/\" r
let p, q, r be Element of L9; :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by ;
thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A49
.= minreal . (p,(minreal . (q,r))) by A49
.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4
.= minreal . ((p "/\" q),r) by A49
.= (p "/\" q) "/\" r by A49 ; :: thesis: verum
end;
now :: thesis: for p, q, r being Element of L9 holds p "\/" (q "\/" r) = (p "\/" q) "\/" r
let p, q, r be Element of L9; :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by ;
thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A49
.= maxreal . (p,(maxreal . (q,r))) by A49
.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3
.= maxreal . ((p "\/" q),r) by A49
.= (p "\/" q) "\/" r by A49 ; :: thesis: verum
end;
then ( L9 is join-commutative & L9 is join-associative & L9 is meet-absorbing & L9 is meet-commutative & L9 is meet-associative & L9 is join-absorbing ) by ;
then reconsider L9 = L9 as Lattice ;
reconsider L9 = L9 as SubLattice of RealSubLatt ((In (0,REAL)),(In (1,REAL))) by ;
take L9 ; :: thesis: ( L9 is \/-inheriting & not L9 is /\-inheriting )
now :: thesis: for X being Subset of L9 holds "\/" (X,L) in the carrier of L9
let X be Subset of L9; :: thesis: "\/" (X,L) in the carrier of L9
thus "\/" (X,L) in the carrier of L9 :: thesis: verum
proof
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider w = 0 as Element of L by ;
A56: X is_less_than "\/" (X,L) by LATTICE3:def 21;
"\/" (X,L) in [.0,1.] by A13;
then "\/" (X,L) in { r where r is Real : ( 0 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider y being Real such that
A57: y = "\/" (X,L) and
0 <= y and
A58: y <= 1 ;
reconsider y = y as Real ;
assume A59: not "\/" (X,L) in the carrier of L9 ; :: thesis: contradiction
then not "\/" (X,L) in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } by ;
then A60: y <= 1 / 2 by ;
now :: thesis: for z9 being object st z9 in X holds
z9 in
let z9 be object ; :: thesis: ( z9 in X implies z9 in )
assume A61: z9 in X ; :: thesis: z9 in
then reconsider z = z9 as Element of L9 ;
reconsider z = z as Element of L by ;
A62: z [= "\/" (X,L) by ;
reconsider z1 = z as Real ;
reconsider z1 = z1 as Real ;
min (z1,y) = minreal . (z1,("\/" (X,L))) by
.= () . [z,("\/" (X,L))] by
.= () . (z,("\/" (X,L)))
.= z "/\" ("\/" (X,L)) by
.= z1 by ;
then z1 <= y by XXREAL_0:def 9;
then y + z1 <= (1 / 2) + y by ;
then for v being Real holds
( not z1 = v or not 1 / 2 < v or not v <= 1 ) by XREAL_1:6;
then not z1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ;
hence z9 in by ; :: thesis: verum
end;
then A63: X c= ;
per cases ( X = {} or X = ) by ;
suppose A64: X = {} ; :: thesis: contradiction
A65: now :: thesis: for r1 being Element of L st X is_less_than r1 holds
w [= r1
let r1 be Element of L; :: thesis: ( X is_less_than r1 implies w [= r1 )
assume X is_less_than r1 ; :: thesis: w [= r1
r1 in [.0,1.] by A13;
then r1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider e being Real such that
A66: r1 = e and
A67: 0 <= e and
e <= 1 ;
reconsider e = e as Real ;
w "/\" r1 = () . (w,r1) by
.= minreal . [w,r1] by
.= minreal . (w,r1)
.= min (0,e) by
.= w by ;
hence w [= r1 by LATTICES:4; :: thesis: verum
end;
for q being Element of L st q in X holds
q [= w by A64;
then X is_less_than w ;
then "\/" (X,L) = w by ;
then "\/" (X,L) in by TARSKI:def 1;
hence contradiction by A9, A59, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
hence L9 is \/-inheriting ; :: thesis: not L9 is /\-inheriting
now :: thesis: not for X being Subset of L9 holds "/\" (X,L) in the carrier of L9
1 / 2 in { x where x is Real : ( 0 <= x & x <= 1 ) } ;
then reconsider z = 1 / 2 as Element of L by ;
set X = { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ;
for y being Real holds
( not y = 1 / 2 or not 1 / 2 < y or not y <= 1 ) ;
then A68: ( not 1 / 2 in & not 1 / 2 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } ) by TARSKI:def 1;
for x1 being object st x1 in { x where x is Real : ( 1 / 2 < x & x <= 1 ) } holds
x1 in B by ;
then reconsider X = { x where x is Real : ( 1 / 2 < x & x <= 1 ) } as Subset of L9 by TARSKI:def 3;
take X = X; :: thesis: not "/\" (X,L) in the carrier of L9
A69: now :: thesis: for b being Element of L st b is_less_than X holds
b [= z
let b be Element of L; :: thesis: ( b is_less_than X implies b [= z )
b in A by A13;
then b in { r where r is Real : ( 0 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider b9 being Real such that
A70: b = b9 and
A71: 0 <= b9 and
A72: b9 <= 1 ;
reconsider b9 = b9 as Real ;
assume A73: b is_less_than X ; :: thesis: b [= z
A74: b9 <= 1 / 2
proof
assume A75: 1 / 2 < b9 ; :: thesis: contradiction
then b9 in X by A72;
then A76: b = "/\" (X,L) by ;
(1 / 2) + b9 < b9 + b9 by ;
then A77: ((1 / 2) + b9) / 2 < (b9 + b9) / 2 by XREAL_1:74;
then (((1 / 2) + b9) / 2) + b9 <= b9 + 1 by ;
then A78: ((1 / 2) + b9) / 2 <= 1 by XREAL_1:6;
then ((1 / 2) + b9) / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A71;
then reconsider c = ((1 / 2) + b9) / 2 as Element of L by ;
reconsider cc = c as Real ;
(1 / 2) + (1 / 2) < b9 + (1 / 2) by ;
then 1 / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;
then ((1 / 2) + b9) / 2 in X by A78;
then b [= c by ;
then b9 = b "/\" c by
.= () . (b,c) by
.= minreal . [b,c] by
.= minreal . (b,cc)
.= min (b9,(((1 / 2) + b9) / 2)) by ;
hence contradiction by A77, XXREAL_0:def 9; :: thesis: verum
end;
b "/\" z = () . (b,z) by
.= minreal . [b,z] by
.= minreal . (b,z)
.= min (b9,jd) by
.= b by ;
hence b [= z by LATTICES:4; :: thesis: verum
end;
now :: thesis: for q being Element of L st q in X holds
z [= q
let q be Element of L; :: thesis: ( q in X implies z [= q )
assume q in X ; :: thesis: z [= q
then A79: ex y being Real st
( q = y & 1 / 2 < y & y <= 1 ) ;
q in A by A13;
then q in { r where r is Real : ( 0 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider q9 being Real such that
A80: q = q9 and
0 <= q9 and
q9 <= 1 ;
reconsider q9 = q9 as Real ;
z "/\" q = () . (z,q) by
.= minreal . [z,q] by
.= minreal . (z,q)
.= min (jd,q9) by
.= z by ;
hence z [= q by LATTICES:4; :: thesis: verum
end;
then z is_less_than X ;
then "/\" (X,L) = jd by ;
hence not "/\" (X,L) in the carrier of L9 by ; :: thesis: verum
end;
hence not L9 is /\-inheriting ; :: thesis: verum