set R = Real_Lattice ;
A1: 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;
set L = RealSubLatt 0 ,1;
A2: ( A = the carrier of (RealSubLatt 0 ,1) & the L_join of (RealSubLatt 0 ,1) = maxreal || [.0 ,1.] & the L_meet of (RealSubLatt 0 ,1) = minreal || [.0 ,1.] ) by Def4;
set Ma = maxreal || A;
set Mi = minreal || A;
reconsider Ma = maxreal || A, Mi = minreal || A as BinOp of A by A2;
reconsider L = RealSubLatt 0 ,1 as complete Lattice by Th21;
set B = {0 ,1} \/ ].0 ,(1 / 2).[;
A3: {0 ,1} \/ ].0 ,(1 / 2).[ = {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) }

proof

thus {0 ,1} \/ ].0 ,(1 / 2).[ c= {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } :: according to XBOOLE_0:def 10 :: thesis: {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 {0 ,1} \/ ].0 ,(1 / 2).[ or x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } )
assume A4: 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 A4, 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
A5: ( x1 = y & 0 < y & y < 1 / 2 ) ;
y in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A5;
hence x1 in {1} \/ { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } by A5, 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;

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

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 A6: 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 A6, 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
A7: ( x1 = y & 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 A7, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

end;

end;

reconsider B = {0 ,1} \/ ].0 ,(1 / 2).[ as non empty set ;

A8: now

let x1 be set ; :: thesis: ( x1 in B implies x1 in A )
assume A9: 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 A3, A9, XBOOLE_0:def 3;

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

then x1 = 1 by TARSKI:def 1;
hence x1 in A by A1, 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
A10: ( x1 = y & 0 <= y & y < 1 / 2 ) ;
y + (1 / 2) <= (1 / 2) + 1 by A10, XREAL_1:9;
then y <= 1 by XREAL_1:8;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A10;
hence x1 in A by RCOMP_1:def 1; :: thesis: verum

end;

end;

end;

hence x1 in A ; :: thesis: verum

end;

then A11: B c= A by TARSKI:def 3;
then A12: [: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;
A13: ( dom ma = [:B,B:] & dom mi = [:B,B:] ) by FUNCT_2:def 1;

now

let x' be set ; :: thesis: ( x' in dom ma implies ma . x' in B )
assume A14: x' in dom ma ; :: thesis: ma . x' in B
then consider x1, x2 being set such that
A15: x' = [x1,x2] by RELAT_1:def 1;
A16: ( x1 in B & x2 in B ) by A14, A15, ZFMISC_1:106;

now

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

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

then A17: 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 A3, A16, XBOOLE_0:def 3;

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

then A18: x2 = 1 by TARSKI:def 1;
ma . x' = Ma . [x1,x2] by A14, A15, FUNCT_1:72
.= maxreal . x1,x2 by A12, A13, A14, A15, FUNCT_1:72
.= max 1,1 by A17, A18, REAL_LAT:def 2
.= 1 ;
then ma . x' in {1} by TARSKI:def 1;
hence ma . x' in B by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider y2 being Element of REAL such that
A19: ( x2 = y2 & 0 <= y2 & y2 < 1 / 2 ) ;
ma . x' = Ma . [x1,x2] by A14, A15, FUNCT_1:72
.= maxreal . x1,x2 by A12, A13, A14, A15, FUNCT_1:72
.= max 1,y2 by A17, A19, REAL_LAT:def 2 ;
then ( ma . x' = 1 or ma . x' = y2 ) by XXREAL_0:16;
then ( ma . x' in {1} or ma . x' in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A19, TARSKI:def 1;
hence ma . x' in B by A3, 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 : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: ma . x' in B

then consider y1 being Element of REAL such that
A20: ( x1 = y1 & 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 A3, A16, XBOOLE_0:def 3;

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

then A21: x2 = 1 by TARSKI:def 1;
ma . x' = Ma . [x1,x2] by A14, A15, FUNCT_1:72
.= maxreal . x1,x2 by A12, A13, A14, A15, FUNCT_1:72
.= max y1,1 by A20, A21, REAL_LAT:def 2 ;
then ( ma . x' = y1 or ma . x' = 1 ) by XXREAL_0:16;
then ( ma . x' in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } or ma . x' in {1} ) by A20, TARSKI:def 1;
hence ma . x' in B by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider y2 being Element of REAL such that
A22: ( x2 = y2 & 0 <= y2 & y2 < 1 / 2 ) ;
ma . x' = Ma . [x1,x2] by A14, A15, FUNCT_1:72
.= maxreal . x1,x2 by A12, A13, A14, A15, FUNCT_1:72
.= max y1,y2 by A20, A22, 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 : ( 0 <= x & x < 1 / 2 ) } by A20, A22;
hence ma . x' in B by A3, 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;

then reconsider ma = ma as BinOp of B by A13, FUNCT_2:5;

now

let x' be set ; :: thesis: ( x' in dom mi implies mi . x' in B )
assume A23: x' in dom mi ; :: thesis: mi . x' in B
then consider x1, x2 being set such that
A24: x' = [x1,x2] by RELAT_1:def 1;
A25: ( x1 in B & x2 in B ) by A23, A24, ZFMISC_1:106;

now

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

suppose x1 in {1} ; :: thesis: mi . x' 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 A3, A25, XBOOLE_0:def 3;

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

then A27: x2 = 1 by TARSKI:def 1;
mi . x' = Mi . [x1,x2] by A23, A24, FUNCT_1:72
.= minreal . x1,x2 by A12, A13, A23, A24, FUNCT_1:72
.= min 1,1 by A26, A27, REAL_LAT:def 1
.= 1 ;
then mi . x' in {1} by TARSKI:def 1;
hence mi . x' in B by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider y2 being Element of REAL such that
A28: ( x2 = y2 & 0 <= y2 & y2 < 1 / 2 ) ;
mi . x' = Mi . [x1,x2] by A23, A24, FUNCT_1:72
.= minreal . x1,x2 by A12, A13, A23, A24, FUNCT_1:72
.= min 1,y2 by A26, A28, REAL_LAT:def 1 ;
then ( mi . x' = 1 or mi . x' = y2 ) by XXREAL_0:15;
then ( mi . x' in {1} or mi . x' in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A28, TARSKI:def 1;
hence mi . x' in B by A3, 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 : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: mi . x' in B

then consider y1 being Element of REAL such that
A29: ( x1 = y1 & 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 A3, A25, XBOOLE_0:def 3;

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

then A30: x2 = 1 by TARSKI:def 1;
mi . x' = Mi . [x1,x2] by A23, A24, FUNCT_1:72
.= minreal . x1,x2 by A12, A13, A23, A24, FUNCT_1:72
.= min y1,1 by A29, A30, REAL_LAT:def 1 ;
then ( mi . x' = y1 or mi . x' = 1 ) by XXREAL_0:15;
then ( mi . x' in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } or mi . x' in {1} ) by A29, TARSKI:def 1;
hence mi . x' in B by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then consider y2 being Element of REAL such that
A31: ( x2 = y2 & 0 <= y2 & y2 < 1 / 2 ) ;
mi . x' = Mi . [x1,x2] by A23, A24, FUNCT_1:72
.= minreal . x1,x2 by A12, A13, A23, A24, FUNCT_1:72
.= min y1,y2 by A29, A31, 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 : ( 0 <= x & x < 1 / 2 ) } by A29, A31;
hence mi . x' in B by A3, 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;

then reconsider mi = mi as BinOp of B by A13, FUNCT_2:5;
reconsider L' = LattStr(# B,ma,mi #) as non empty LattStr ;

A32: 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 consider y1 being Element of REAL such that
A33: ( x1 = y1 & 0 <= y1 & y1 <= 1 ) ;
thus x1 is Element of Real_Lattice by A33, REAL_LAT:def 4; :: thesis: verum

end;

A34: 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 A3, 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 A1, A2, 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
A35: ( x1 = y & 0 <= y & y < 1 / 2 ) ;
y + (1 / 2) <= (1 / 2) + 1 by A35, XREAL_1:9;
then y <= 1 by XREAL_1:8;
then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A35;
hence x1 is Element of L by A2, RCOMP_1:def 1; :: thesis: verum

end;

end;

end;

A36: now

let a, b be Element of L'; :: thesis: ( a "\/" b = maxreal . a,b & a "/\" b = minreal . a,b )
A37: [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 A12, A37, 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 A12, A37, FUNCT_1:72 ; :: thesis: verum

end;

A38: now

let p, q be Element of L'; :: thesis: p "\/" q = q "\/" p
reconsider p' = p, q' = q as Element of L by A34;
reconsider p' = p', q' = q' as Element of Real_Lattice by A2, A32;
thus p "\/" q = maxreal . p,q by A36
.= maxreal . q',p' by REAL_LAT:8
.= q "\/" p by A36 ; :: thesis: verum

end;

A39: now

let p, q, r be Element of L'; :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
reconsider p' = p, q' = q, r' = r as Element of L by A34;
reconsider p' = p', q' = q', r' = r' as Element of Real_Lattice by A2, A32;
thus p "\/" (q "\/" r) = maxreal . p,(q "\/" r) by A36
.= maxreal . p,(maxreal . q,r) by A36
.= maxreal . (maxreal . p',q'),r' by REAL_LAT:10
.= maxreal . (p "\/" q),r by A36
.= (p "\/" q) "\/" r by A36 ; :: thesis: verum

end;

A40: now

let p, q be Element of L'; :: thesis: (p "/\" q) "\/" q = q
reconsider p' = p, q' = q as Element of L by A34;
reconsider p' = p', q' = q' as Element of Real_Lattice by A2, A32;
thus (p "/\" q) "\/" q = maxreal . (p "/\" q),q by A36
.= maxreal . (minreal . p',q'),q' by A36
.= q by REAL_LAT:12 ; :: thesis: verum

end;

A41: now

let p, q be Element of L'; :: thesis: p "/\" q = q "/\" p
reconsider p' = p, q' = q as Element of L by A34;
reconsider p' = p', q' = q' as Element of Real_Lattice by A2, A32;
thus p "/\" q = minreal . p,q by A36
.= minreal . q',p' by REAL_LAT:9
.= q "/\" p by A36 ; :: thesis: verum

end;

A42: now

let p, q, r be Element of L'; :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
reconsider p' = p, q' = q, r' = r as Element of L by A34;
reconsider p' = p', q' = q', r' = r' as Element of Real_Lattice by A2, A32;
thus p "/\" (q "/\" r) = minreal . p,(q "/\" r) by A36
.= minreal . p,(minreal . q,r) by A36
.= minreal . (minreal . p',q'),r' by REAL_LAT:11
.= minreal . (p "/\" q),r by A36
.= (p "/\" q) "/\" r by A36 ; :: thesis: verum

end;

now

let p, q be Element of L'; :: thesis: p "/\" (p "\/" q) = p
reconsider p' = p, q' = q as Element of L by A34;
reconsider p' = p', q' = q' as Element of Real_Lattice by A2, A32;
thus p "/\" (p "\/" q) = minreal . p,(p "\/" q) by A36
.= minreal . p',(maxreal . p',q') by A36
.= p by REAL_LAT:13 ; :: 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 A38, A39, A40, A41, A42, 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 A2, A11, NAT_LAT:def 16;
take L' ; :: thesis: ( L' is /\-inheriting & not L' is \/-inheriting )

now

let X be Subset of L'; :: thesis: "/\" X,L in the carrier of L'
thus "/\" X,L in the carrier of L' :: thesis: verum

proof

"/\" X,L in [.0 ,1.] by A2;
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
A43: ( y = "/\" X,L & 0 <= y & y <= 1 ) ;
A44: "/\" X,L is_less_than X by LATTICE3:34;
assume A45: not "/\" X,L in the carrier of L' ; :: thesis: contradiction
then ( not "/\" X,L in {1} & not "/\" X,L in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ) by A3, XBOOLE_0:def 3;
then A46: 1 / 2 <= y by A43;

now

let z' be set ; :: thesis: ( z' in X implies z' in {1} )
assume A47: z' in X ; :: thesis: z' in {1}
then reconsider z = z' as Element of L' ;
reconsider z = z as Element of L by A2, A8;
reconsider z1 = z as Element of REAL by TARSKI:def 3;
A48: "/\" X,L [= z by A44, A47, LATTICE3:def 16;
min z1,y = minreal . z,("/\" X,L) by A43, REAL_LAT:def 1
.= (minreal || A) . [z,("/\" X,L)] by A2, FUNCT_1:72
.= (minreal || A) . z,("/\" X,L)
.= z "/\" ("/\" X,L) by A2, LATTICES:def 2
.= y by A43, A48, LATTICES:21 ;
then y <= z1 by XXREAL_0:def 9;
then y + (1 / 2) <= z1 + y by A46, XREAL_1:9;
then for v being Element of REAL holds
( not z1 = v or not 0 <= v or not v < 1 / 2 ) by XREAL_1:8;
then not z1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ;
hence z' in {1} by A3, XBOOLE_0:def 3; :: thesis: verum

end;

then A49: X c= {1} by TARSKI:def 3;
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider w = 1 as Element of L by A2, RCOMP_1:def 1;

now

per cases ( X = {} or X = {1} ) by A49, ZFMISC_1:39;

suppose X = {} ; :: thesis: contradiction

then for q being Element of L st q in X holds
w [= q ;
then A50: w is_less_than X by LATTICE3:def 16;

now

let r1 be Element of L; :: thesis: ( r1 is_less_than X implies r1 [= w )
r1 in [.0 ,1.] by A2;
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
A51: ( r1 = e & 0 <= e & e <= 1 ) ;
assume r1 is_less_than X ; :: thesis: r1 [= w
r1 "/\" w = (minreal || A) . r1,w by A2, LATTICES:def 2
.= minreal . [r1,w] by A2, FUNCT_1:72
.= minreal . r1,w
.= min e,1 by A51, REAL_LAT:def 1
.= r1 by A51, XXREAL_0:def 9 ;
hence r1 [= w by LATTICES:21; :: thesis: verum

end;

then "/\" X,L = w by A50, LATTICE3:34;
then "/\" X,L in {1} by TARSKI:def 1;
hence contradiction by A3, A45, XBOOLE_0:def 3; :: thesis: verum

end;

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

then "/\" X,L = w by LATTICE3:43;
then "/\" X,L in {1} by TARSKI:def 1;
hence contradiction by A3, A45, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

hence L' is /\-inheriting by Def2; :: thesis: not L' is \/-inheriting

now

set X = { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ;
for x1 being set st x1 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } holds
x1 in B by A3, XBOOLE_0:def 3;
then reconsider X = { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } as Subset of L' by TARSKI:def 3;
take X = X; :: thesis: not "\/" X,L in the carrier of L'
1 / 2 in { x where x is Element of REAL : ( 0 <= x & x <= 1 ) } ;
then reconsider z = 1 / 2 as Element of L by A2, RCOMP_1:def 1;

now

let q be Element of L; :: thesis: ( q in X implies q [= z )
q in A by A2;
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
A52: ( q = q' & 0 <= q' & q' <= 1 ) ;
assume q in X ; :: thesis: q [= z
then consider y being Element of REAL such that
A53: ( q = y & 0 <= y & y < 1 / 2 ) ;
q "/\" z = (minreal || A) . q,z by A2, LATTICES:def 2
.= minreal . [q,z] by A2, FUNCT_1:72
.= minreal . q,z
.= min q',(1 / 2) by A52, REAL_LAT:def 1
.= q by A52, A53, XXREAL_0:def 9 ;
hence q [= z by LATTICES:21; :: thesis: verum

end;

then A54: X is_less_than z by LATTICE3:def 17;

now

let b be Element of L; :: thesis: ( X is_less_than b implies z [= b )
b in A by A2;
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
A55: ( b = b' & 0 <= b' & b' <= 1 ) ;
assume A56: X is_less_than b ; :: thesis: z [= b
A57: 1 / 2 <= b'

proof

assume A58: b' < 1 / 2 ; :: thesis: contradiction
then b' + b' < (1 / 2) + b' by XREAL_1:8;
then A59: (b' + b') / 2 < ((1 / 2) + b') / 2 by XREAL_1:76;
(1 / 2) + b' <= 1 + 1 by A55, XREAL_1:9;
then ((1 / 2) + b') / 2 <= (1 + 1) / 2 by XREAL_1:74;
then ((1 / 2) + b') / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A55;
then reconsider c = ((1 / 2) + b') / 2 as Element of L by A2, RCOMP_1:def 1;
b' + (1 / 2) < (1 / 2) + (1 / 2) by A58, XREAL_1:8;
then ((1 / 2) + b') / 2 < 1 / 2 by XREAL_1:76;
then A60: ((1 / 2) + b') / 2 in X by A55;
b' in X by A55, A58;
then b = "\/" X,L by A55, A56, LATTICE3:41;
then c [= b by A60, LATTICE3:38;
then ((1 / 2) + b') / 2 = c "/\" b by LATTICES:21
.= (minreal || A) . c,b by A2, LATTICES:def 2
.= minreal . [c,b] by A2, FUNCT_1:72
.= minreal . c,b
.= min (((1 / 2) + b') / 2),b' by A55, REAL_LAT:def 1 ;
hence contradiction by A59, XXREAL_0:def 9; :: thesis: verum

end;

z "/\" b = (minreal || A) . z,b by A2, LATTICES:def 2
.= minreal . [z,b] by A2, FUNCT_1:72
.= minreal . z,b
.= min (1 / 2),b' by A55, REAL_LAT:def 1
.= z by A57, XXREAL_0:def 9 ;
hence z [= b by LATTICES:21; :: thesis: verum

end;

then A61: "\/" X,L = 1 / 2 by A54, LATTICE3:def 21;
A62: not 1 / 2 in {1} by TARSKI:def 1;
for y being Element of REAL holds
( not y = 1 / 2 or not 0 <= y or not y < 1 / 2 ) ;
then not 1 / 2 in { x where x is Element of REAL : ( 0 <= x & x < 1 / 2 ) } ;
hence not "\/" X,L in the carrier of L' by A3, A61, A62, XBOOLE_0:def 3; :: thesis: verum

end;

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