set B = {0,1} \/ ].0,(1 / 2).[;
set L = RealSubLatt (0,1);
set R = Real_Lattice ;
A1: {0,1} \/ ].0,(1 / 2).[ c= {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) }

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {0,1} \/ ].0,(1 / 2).[ or x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } )
assume A2: x1 in {0,1} \/ ].0,(1 / 2).[ ; :: thesis: x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) }

now

per cases ( x1 in {0,1} or x1 in ].0,(1 / 2).[ ) by A2, XBOOLE_0:def 3;

suppose x1 in {0,1} ; :: thesis: x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) }

then ( x1 = 0 or x1 = 1 ) by TARSKI:def 2;
then ( x1 in {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;
hence x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x1 in ].0,(1 / 2).[ ; :: thesis: x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) }

then x1 in { r where r is Real : ( 0 < r & r < 1 / 2 ) } by RCOMP_1:def 2;
then consider y being Element of REAL such that
A3: x1 = y and
A4: ( 0 < y & y < 1 / 2 ) ;
y in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A4;
hence x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: verum

end;

{1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } c= {0,1} \/ ].0,(1 / 2).[

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } or x1 in {0,1} \/ ].0,(1 / 2).[ )
assume A5: x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: x1 in {0,1} \/ ].0,(1 / 2).[

now

per cases ( x1 in {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A5, XBOOLE_0:def 3;

suppose x1 in {1} ; :: thesis: x1 in {0,1} \/ ].0,(1 / 2).[

then x1 = 1 by TARSKI:def 1;
then x1 in {0,1} by TARSKI:def 2;
hence x1 in {0,1} \/ ].0,(1 / 2).[ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: x1 in {0,1} \/ ].0,(1 / 2).[

then consider y being Element of REAL such that
A6: x1 = y and
A7: ( 0 <= y & y < 1 / 2 ) ;
( y in { r where r is Real : ( 0 < r & r < 1 / 2 ) } or y = 0 ) by A7;
then ( y in ].0,(1 / 2).[ or y in {0,1} ) by RCOMP_1:def 2, TARSKI:def 2;
hence x1 in {0,1} \/ ].0,(1 / 2).[ by A6, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x1 in {0,1} \/ ].0,(1 / 2).[ ; :: thesis: verum

end;

then A8: {0,1} \/ ].0,(1 / 2).[ = {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A1, XBOOLE_0:def 10;
A9: 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider A = [.0,1.] as non empty set by RCOMP_1:def 1;

A10: now

let x1 be Element of A; :: thesis: x1 is Element of Real_Lattice
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 Real_Lattice by REAL_LAT:def 3; :: thesis: verum

end;

reconsider B = {0,1} \/ ].0,(1 / 2).[ as non empty set ;
A11: the L_meet of (RealSubLatt (0,1)) = minreal || [.0,1.] by Def4;
set Ma = maxreal || A;
set Mi = minreal || A;
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 {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A15, XBOOLE_0:def 3;

suppose x1 in {1} ; :: thesis: x1 in A

then x1 = 1 by TARSKI:def 1;
hence x1 in A by A9, RCOMP_1:def 1; :: thesis: verum

end;

suppose x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: x1 in A

then consider y being Element of REAL such that
A16: ( x1 = y & 0 <= y ) and
A17: y < 1 / 2 ;
y + (1 / 2) <= (1 / 2) + 1 by A17, XREAL_1:7;
then y <= 1 by XREAL_1:6;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A16;
hence x1 in A by RCOMP_1:def 1; :: thesis: verum

end;

end;

end;

hence x1 in A ; :: thesis: verum

end;

then A18: B c= A by TARSKI:def 3;
then A19: [: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;
A20: dom ma = [:B,B:] by FUNCT_2:def 1;

A21: now

let x9 be set ; :: thesis: ( x9 in dom ma implies ma . x9 in B )
assume A22: x9 in dom ma ; :: thesis: ma . x9 in B
then consider x1, x2 being set such that
A23: x9 = [x1,x2] by RELAT_1:def 1;
A24: x2 in B by A22, A23, ZFMISC_1:87;
A25: x1 in B by A22, A23, ZFMISC_1:87;

now

per cases ( x1 in {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A25, XBOOLE_0:def 3;

suppose x1 in {1} ; :: thesis: ma . x9 in B

then A26: x1 = 1 by TARSKI:def 1;

now

per cases ( x2 in {1} or x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A24, XBOOLE_0:def 3;

suppose x2 in {1} ; :: thesis: ma . x9 in B

then A27: x2 = 1 by TARSKI:def 1;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (1,1) by A26, A27, REAL_LAT:def 2
.= 1 ;
then ma . x9 in {1} by TARSKI:def 1;
hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: ma . x9 in B

then consider y2 being Element of REAL such that
A28: x2 = y2 and
A29: ( 0 <= y2 & y2 < 1 / 2 ) ;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (1,y2) by A26, A28, REAL_LAT:def 2 ;
then ( ma . x9 = 1 or ma . x9 = y2 ) by XXREAL_0:16;
then ( ma . x9 in {1} or ma . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A29, TARSKI:def 1;
hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ma . x9 in B ; :: thesis: verum

end;

suppose x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: ma . x9 in B

then consider y1 being Element of REAL such that
A30: x1 = y1 and
A31: ( 0 <= y1 & y1 < 1 / 2 ) ;

now

per cases ( x2 in {1} or x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A24, XBOOLE_0:def 3;

suppose x2 in {1} ; :: thesis: ma . x9 in B

then A32: x2 = 1 by TARSKI:def 1;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (y1,1) by A30, A32, REAL_LAT:def 2 ;
then ( ma . x9 = y1 or ma . x9 = 1 ) by XXREAL_0:16;
then ( ma . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } or ma . x9 in {1} ) by A31, TARSKI:def 1;
hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: ma . x9 in B

then consider y2 being Element of REAL such that
A33: x2 = y2 and
A34: ( 0 <= y2 & y2 < 1 / 2 ) ;
ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49
.= maxreal . (x1,x2) by A19, A20, A22, A23, FUNCT_1:49
.= max (y1,y2) by A30, A33, REAL_LAT:def 2 ;
then ( ma . x9 = y1 or ma . x9 = y2 ) by XXREAL_0:16;
then ma . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A31, A34;
hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ma . x9 in B ; :: thesis: verum

end;

end;

end;

hence ma . x9 in B ; :: thesis: verum

end;

A35: dom mi = [:B,B:] by FUNCT_2:def 1;

A36: now

let x9 be set ; :: thesis: ( x9 in dom mi implies mi . x9 in B )
assume A37: x9 in dom mi ; :: thesis: mi . x9 in B
then consider x1, x2 being set such that
A38: x9 = [x1,x2] by RELAT_1:def 1;
A39: x2 in B by A37, A38, ZFMISC_1:87;
A40: x1 in B by A37, A38, ZFMISC_1:87;

now

per cases ( x1 in {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A40, XBOOLE_0:def 3;

suppose x1 in {1} ; :: thesis: mi . x9 in B

then A41: x1 = 1 by TARSKI:def 1;

now

per cases ( x2 in {1} or x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A39, XBOOLE_0:def 3;

suppose x2 in {1} ; :: thesis: mi . x9 in B

then A42: x2 = 1 by TARSKI:def 1;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (1,1) by A41, A42, REAL_LAT:def 1
.= 1 ;
then mi . x9 in {1} by TARSKI:def 1;
hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: mi . x9 in B

then consider y2 being Element of REAL such that
A43: x2 = y2 and
A44: ( 0 <= y2 & y2 < 1 / 2 ) ;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (1,y2) by A41, A43, REAL_LAT:def 1 ;
then ( mi . x9 = 1 or mi . x9 = y2 ) by XXREAL_0:15;
then ( mi . x9 in {1} or mi . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A44, TARSKI:def 1;
hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence mi . x9 in B ; :: thesis: verum

end;

suppose x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: mi . x9 in B

then consider y1 being Element of REAL such that
A45: x1 = y1 and
A46: ( 0 <= y1 & y1 < 1 / 2 ) ;

now

per cases ( x2 in {1} or x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A1, A39, XBOOLE_0:def 3;

suppose x2 in {1} ; :: thesis: mi . x9 in B

then A47: x2 = 1 by TARSKI:def 1;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (y1,1) by A45, A47, REAL_LAT:def 1 ;
then ( mi . x9 = y1 or mi . x9 = 1 ) by XXREAL_0:15;
then ( mi . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } or mi . x9 in {1} ) by A46, TARSKI:def 1;
hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: mi . x9 in B

then consider y2 being Element of REAL such that
A48: x2 = y2 and
A49: ( 0 <= y2 & y2 < 1 / 2 ) ;
mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49
.= minreal . (x1,x2) by A19, A35, A37, A38, FUNCT_1:49
.= min (y1,y2) by A45, A48, REAL_LAT:def 1 ;
then ( mi . x9 = y1 or mi . x9 = y2 ) by XXREAL_0:15;
then mi . x9 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A46, A49;
hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence mi . x9 in B ; :: thesis: verum

end;

end;

end;

hence mi . x9 in B ; :: thesis: verum

end;

reconsider L = RealSubLatt (0,1) as complete Lattice by Th21;
reconsider mi = mi as BinOp of B by A35, A36, FUNCT_2:3;
reconsider ma = ma as BinOp of B by A20, A21, FUNCT_2:3;
reconsider L9 = LattStr(# B,ma,mi #) as non empty LattStr ;

A50: now

let a, b be Element of L9; :: thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )
A51: [a,b] in [:B,B:] ;
thus a "\/" b = the L_join of L9 . (a,b) by LATTICES:def 1
.= (maxreal || A) . [a,b] by FUNCT_1:49
.= maxreal . (a,b) by A19, A51, FUNCT_1:49 ; :: thesis: a "/\" b = minreal . (a,b)
thus a "/\" b = the L_meet of L9 . (a,b) by LATTICES:def 2
.= (minreal || A) . [a,b] by FUNCT_1:49
.= minreal . (a,b) by A19, A51, FUNCT_1:49 ; :: thesis: verum

end;

A52: now

let x1 be Element of B; :: thesis: b₁ is Element of L

per cases ( x1 in {1} or x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A8, XBOOLE_0:def 3;

suppose x1 in {1} ; :: thesis: b₁ is Element of L

then x1 = 1 by TARSKI:def 1;
hence x1 is Element of L by A9, A13, RCOMP_1:def 1; :: thesis: verum

end;

suppose x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: b₁ is Element of L

then consider y being Element of REAL such that
A53: ( x1 = y & 0 <= y ) and
A54: y < 1 / 2 ;
y + (1 / 2) <= (1 / 2) + 1 by A54, XREAL_1:7;
then y <= 1 by XREAL_1:6;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A53;
hence x1 is Element of L by A13, RCOMP_1:def 1; :: thesis: verum

end;

end;

end;

A55: now

let p, q be Element of L9; :: thesis: p "\/" q = q "\/" p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "\/" q = maxreal . (p,q) by A50
.= maxreal . (q9,p9) by REAL_LAT:1
.= q "\/" p by A50 ; :: thesis: verum

end;

A56: now

let p, q be Element of L9; :: thesis: p "/\" (p "\/" q) = p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A50
.= minreal . (p9,(maxreal . (p9,q9))) by A50
.= p by REAL_LAT:6 ; :: thesis: verum

end;

A57: now

let p, q be Element of L9; :: thesis: p "/\" q = q "/\" p
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus p "/\" q = minreal . (p,q) by A50
.= minreal . (q9,p9) by REAL_LAT:2
.= q "/\" p by A50 ; :: thesis: verum

end;

A58: now

let p, q be Element of L9; :: thesis: (p "/\" q) "\/" q = q
reconsider p9 = p, q9 = q as Element of L by A52;
reconsider p9 = p9, q9 = q9 as Element of Real_Lattice by A13, A10;
thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A50
.= maxreal . ((minreal . (p9,q9)),q9) by A50
.= q by REAL_LAT:5 ; :: thesis: verum

end;

A59: now

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 A52;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A10;
thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A50
.= minreal . (p,(minreal . (q,r))) by A50
.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4
.= minreal . ((p "/\" q),r) by A50
.= (p "/\" q) "/\" r by A50 ; :: thesis: verum

end;

now

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 A52;
reconsider p9 = p9, q9 = q9, r9 = r9 as Element of Real_Lattice by A13, A10;
thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A50
.= maxreal . (p,(maxreal . (q,r))) by A50
.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3
.= maxreal . ((p "\/" q),r) by A50
.= (p "\/" q) "\/" r by A50 ; :: 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 A55, A58, A57, A59, A56, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
then reconsider L9 = L9 as Lattice ;
reconsider L9 = L9 as SubLattice of RealSubLatt (0,1) by A13, A12, A11, A18, NAT_LAT:def 12;
take L9 ; :: thesis: ( L9 is /\-inheriting & not L9 is \/-inheriting )

now

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

1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider w = 1 as Element of L by A13, RCOMP_1:def 1;
A60: "/\" (X,L) is_less_than X by LATTICE3:34;
"/\" (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
A61: y = "/\" (X,L) and
A62: 0 <= y and
y <= 1 ;
assume A63: not "/\" (X,L) in the carrier of L9 ; :: thesis: contradiction
then not "/\" (X,L) in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A8, XBOOLE_0:def 3;
then A64: 1 / 2 <= y by A61, A62;

now

let z9 be set ; :: thesis: ( z9 in X implies z9 in {1} )
assume A65: z9 in X ; :: thesis: z9 in {1}
then reconsider z = z9 as Element of L9 ;
reconsider z = z as Element of L by A13, A14;
A66: "/\" (X,L) [= z by A60, A65, LATTICE3:def 16;
reconsider z1 = z as Element of REAL by TARSKI:def 3;
min (z1,y) = minreal . (z,("/\" (X,L))) by A61, REAL_LAT:def 1
.= (minreal || A) . [z,("/\" (X,L))] by A13, FUNCT_1:49
.= (minreal || A) . (z,("/\" (X,L)))
.= z "/\" ("/\" (X,L)) by A11, LATTICES:def 2
.= y by A61, A66, LATTICES:4 ;
then y <= z1 by XXREAL_0:def 9;
then y + (1 / 2) <= z1 + y by A64, XREAL_1:7;
then for v being Element of REAL holds
( not z1 = v or not 0 <= v or not v < 1 / 2 ) by XREAL_1:6;
then not z1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ;
hence z9 in {1} by A8, XBOOLE_0:def 3; :: thesis: verum

end;

then A67: X c= {1} by TARSKI:def 3;

now

per cases ( X = {} or X = {1} ) by A67, ZFMISC_1:33;

suppose A68: X = {} ; :: thesis: contradiction

A69: now

let r1 be Element of L; :: thesis: ( r1 is_less_than X implies r1 [= w )
assume r1 is_less_than X ; :: thesis: r1 [= w
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
A70: r1 = e and
0 <= e and
A71: e <= 1 ;
r1 "/\" w = (minreal || A) . (r1,w) by A11, LATTICES:def 2
.= minreal . [r1,w] by A13, FUNCT_1:49
.= minreal . (r1,w)
.= min (e,1) by A70, REAL_LAT:def 1
.= r1 by A70, A71, XXREAL_0:def 9 ;
hence r1 [= w by LATTICES:4; :: thesis: verum

end;

for q being Element of L st q in X holds
w [= q by A68;
then w is_less_than X by LATTICE3:def 16;
then "/\" (X,L) = w by A69, LATTICE3:34;
then "/\" (X,L) in {1} by TARSKI:def 1;
hence contradiction by A8, A63, XBOOLE_0:def 3; :: thesis: verum

end;

suppose X = {1} ; :: thesis: contradiction

then "/\" (X,L) = w by LATTICE3:42;
then "/\" (X,L) in {1} by TARSKI:def 1;
hence contradiction by A8, A63, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

hence L9 is /\-inheriting by Def2; :: thesis: not L9 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 L by A13, RCOMP_1:def 1;
set X = { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ;
for y being Element of REAL holds
( not y = 1 / 2 or not 0 <= y or not y < 1 / 2 ) ;
then A72: ( not 1 / 2 in {1} & not 1 / 2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;
for x1 being set st x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } holds
x1 in B by A8, XBOOLE_0:def 3;
then reconsider X = { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } as Subset of L9 by TARSKI:def 3;
take X = X; :: thesis: not "\/" (X,L) in the carrier of L9

A73: now

let b be Element of L; :: thesis: ( X is_less_than b implies z [= b )
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 Element of REAL such that
A74: b = b9 and
A75: 0 <= b9 and
A76: b9 <= 1 ;
assume A77: X is_less_than b ; :: thesis: z [= b
A78: 1 / 2 <= b9

proof

(1 / 2) + b9 <= 1 + 1 by A76, XREAL_1:7;
then ((1 / 2) + b9) / 2 <= (1 + 1) / 2 by XREAL_1:72;
then ((1 / 2) + b9) / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A75;
then reconsider c = ((1 / 2) + b9) / 2 as Element of L by A13, RCOMP_1:def 1;
assume A79: b9 < 1 / 2 ; :: thesis: contradiction
then b9 + b9 < (1 / 2) + b9 by XREAL_1:6;
then A80: (b9 + b9) / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;
b9 + (1 / 2) < (1 / 2) + (1 / 2) by A79, XREAL_1:6;
then ((1 / 2) + b9) / 2 < 1 / 2 by XREAL_1:74;
then A81: ((1 / 2) + b9) / 2 in X by A75;
b9 in X by A75, A79;
then b = "\/" (X,L) by A74, A77, LATTICE3:40;
then c [= b by A81, LATTICE3:38;
then ((1 / 2) + b9) / 2 = c "/\" b by LATTICES:4
.= (minreal || A) . (c,b) by A11, LATTICES:def 2
.= minreal . [c,b] by A13, FUNCT_1:49
.= minreal . (c,b)
.= min ((((1 / 2) + b9) / 2),b9) by A74, REAL_LAT:def 1 ;
hence contradiction by A80, XXREAL_0:def 9; :: thesis: verum

end;

z "/\" b = (minreal || A) . (z,b) by A11, LATTICES:def 2
.= minreal . [z,b] by A13, FUNCT_1:49
.= minreal . (z,b)
.= min ((1 / 2),b9) by A74, REAL_LAT:def 1
.= z by A78, XXREAL_0:def 9 ;
hence z [= b by LATTICES:4; :: thesis: verum

end;

now

let q be Element of L; :: thesis: ( q in X implies q [= z )
assume q in X ; :: thesis: q [= z
then A82: ex y being Element of REAL st
( q = y & 0 <= y & y < 1 / 2 ) ;
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 Element of REAL such that
A83: q = q9 and
0 <= q9 and
q9 <= 1 ;
q "/\" z = (minreal || A) . (q,z) by A11, LATTICES:def 2
.= minreal . [q,z] by A13, FUNCT_1:49
.= minreal . (q,z)
.= min (q9,(1 / 2)) by A83, REAL_LAT:def 1
.= q by A83, A82, XXREAL_0:def 9 ;
hence q [= z by LATTICES:4; :: thesis: verum

end;

then X is_less_than z by LATTICE3:def 17;
then "\/" (X,L) = 1 / 2 by A73, LATTICE3:def 21;
hence not "\/" (X,L) in the carrier of L9 by A1, A72, XBOOLE_0:def 3; :: thesis: verum

end;

hence not L9 is \/-inheriting by Def3; :: thesis: verum