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