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

set L = RealSubLatt ((In (0,REAL)),(In (1,REAL)));

set R = Real_Lattice ;

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

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: for x1 being Element of A holds x1 is Element of Real_Lattice by REAL_LAT:def 3, XREAL_0:def 1;

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

A11: the L_meet of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = minreal || [.0,1.] by Def4;

set Ma = maxreal || A;

set Mi = minreal || A;

A12: the L_join of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = maxreal || [.0,1.] 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;

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;

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 ;

then reconsider L9 = L9 as Lattice ;

reconsider L9 = L9 as SubLattice of RealSubLatt ((In (0,REAL)),(In (1,REAL))) by A13, A12, A11, A18, NAT_LAT:def 12;

take L9 ; :: thesis: ( L9 is /\-inheriting & not L9 is \/-inheriting )

set L = RealSubLatt ((In (0,REAL)),(In (1,REAL)));

set R = Real_Lattice ;

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

proof

{1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } c= {0,1} \/ ].0,(1 / 2).[
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {0,1} \/ ].0,(1 / 2).[ or x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )

assume A2: x1 in {0,1} \/ ].0,(1 / 2).[ ; :: thesis: x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) }

end;assume A2: x1 in {0,1} \/ ].0,(1 / 2).[ ; :: thesis: x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) }

now :: thesis: x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } end;

hence
x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
; :: thesis: verumper cases
( x1 in {0,1} or x1 in ].0,(1 / 2).[ )
by A2, XBOOLE_0:def 3;

end;

suppose
x1 in {0,1}
; :: thesis: x1 in {1} \/ { x where x is 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 Real : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;

hence x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by XBOOLE_0:def 3; :: thesis: verum

end;then ( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;

hence x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by XBOOLE_0:def 3; :: thesis: verum

suppose
x1 in ].0,(1 / 2).[
; :: thesis: x1 in {1} \/ { x where x is 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 Real such that

A3: x1 = y and

A4: ( 0 < y & y < 1 / 2 ) ;

y in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A4;

hence x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A3, XBOOLE_0:def 3; :: thesis: verum

end;then consider y being Real such that

A3: x1 = y and

A4: ( 0 < y & y < 1 / 2 ) ;

y in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A4;

hence x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A3, XBOOLE_0:def 3; :: thesis: verum

proof

then A8:
{0,1} \/ ].0,(1 / 2).[ = {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
by A1, XBOOLE_0:def 10;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } or x1 in {0,1} \/ ].0,(1 / 2).[ )

assume A5: x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: x1 in {0,1} \/ ].0,(1 / 2).[

end;assume A5: x1 in {1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ; :: thesis: x1 in {0,1} \/ ].0,(1 / 2).[

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

hence
x1 in {0,1} \/ ].0,(1 / 2).[
; :: thesis: verumper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A5, XBOOLE_0:def 3;

end;

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;then x1 in {0,1} by TARSKI:def 2;

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

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

then consider y being 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;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

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: for x1 being Element of A holds x1 is Element of Real_Lattice by REAL_LAT:def 3, XREAL_0:def 1;

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

A11: the L_meet of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = minreal || [.0,1.] by Def4;

set Ma = maxreal || A;

set Mi = minreal || A;

A12: the L_join of (RealSubLatt ((In (0,REAL)),(In (1,REAL)))) = maxreal || [.0,1.] 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

then A18:
B c= A
;x1 in A

let x1 be object ; :: thesis: ( x1 in B implies x1 in A )

assume A15: x1 in B ; :: thesis: x1 in A

end;assume A15: x1 in B ; :: thesis: x1 in A

now :: thesis: x1 in Aend;

hence
x1 in A
; :: thesis: verumper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A15, XBOOLE_0:def 3;

end;

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

then consider y being 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;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

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 :: thesis: for x9 being object st x9 in dom ma holds

ma . x9 in B

A35:
dom mi = [:B,B:]
by FUNCT_2:def 1;ma . x9 in B

let x9 be object ; :: 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 object 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;

end;assume A22: x9 in dom ma ; :: thesis: ma . x9 in B

then consider x1, x2 being object 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 :: thesis: ma . x9 in Bend;

hence
ma . x9 in B
; :: thesis: verumper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A25, XBOOLE_0:def 3;

end;

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

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

end;now :: thesis: ma . x9 in Bend;

hence
ma . x9 in B
; :: thesis: verumper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A24, XBOOLE_0:def 3;

end;

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, A22, A23, FUNCT_1:49

.= max (jj,jj) 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;ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, A22, A23, FUNCT_1:49

.= max (jj,jj) 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

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

then consider y2 being Real such that

A28: x2 = y2 and

A29: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, A22, A23, FUNCT_1:49

.= max (jj,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 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;A28: x2 = y2 and

A29: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, A22, A23, FUNCT_1:49

.= max (jj,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 Real : ( 0 <= x & x < 1 / 2 ) } ) by A29, TARSKI:def 1;

hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

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

then consider y1 being Real such that

A30: x1 = y1 and

A31: ( 0 <= y1 & y1 < 1 / 2 ) ;

reconsider y1 = y1 as Real ;

end;A30: x1 = y1 and

A31: ( 0 <= y1 & y1 < 1 / 2 ) ;

reconsider y1 = y1 as Real ;

now :: thesis: ma . x9 in Bend;

hence
ma . x9 in B
; :: thesis: verumper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A24, XBOOLE_0:def 3;

end;

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, A22, A23, FUNCT_1:49

.= max (y1,jj) 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 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;ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, A22, A23, FUNCT_1:49

.= max (y1,jj) 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 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

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

then consider y2 being Real such that

A33: x2 = y2 and

A34: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, 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 Real : ( 0 <= x & x < 1 / 2 ) } by A31, A34;

hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;A33: x2 = y2 and

A34: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

ma . x9 = Ma . [x1,x2] by A22, A23, FUNCT_1:49

.= maxreal . (x1,x2) by A19, 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 Real : ( 0 <= x & x < 1 / 2 ) } by A31, A34;

hence ma . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

A36: now :: thesis: for x9 being object st x9 in dom mi holds

mi . x9 in B

reconsider L = RealSubLatt ((In (0,REAL)),(In (1,REAL))) as complete Lattice by Th20;mi . x9 in B

let x9 be object ; :: 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 object 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;

end;assume A37: x9 in dom mi ; :: thesis: mi . x9 in B

then consider x1, x2 being object 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 :: thesis: mi . x9 in Bend;

hence
mi . x9 in B
; :: thesis: verumper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A40, XBOOLE_0:def 3;

end;

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

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

end;now :: thesis: mi . x9 in Bend;

hence
mi . x9 in B
; :: thesis: verumper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A39, XBOOLE_0:def 3;

end;

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, A37, A38, FUNCT_1:49

.= min (jj,jj) 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;mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, A37, A38, FUNCT_1:49

.= min (jj,jj) 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

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

then consider y2 being Real such that

A43: x2 = y2 and

A44: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, A37, A38, FUNCT_1:49

.= min (jj,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 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;A43: x2 = y2 and

A44: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, A37, A38, FUNCT_1:49

.= min (jj,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 Real : ( 0 <= x & x < 1 / 2 ) } ) by A44, TARSKI:def 1;

hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

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

then consider y1 being Real such that

A45: x1 = y1 and

A46: ( 0 <= y1 & y1 < 1 / 2 ) ;

reconsider y1 = y1 as Real ;

end;A45: x1 = y1 and

A46: ( 0 <= y1 & y1 < 1 / 2 ) ;

reconsider y1 = y1 as Real ;

now :: thesis: mi . x9 in Bend;

hence
mi . x9 in B
; :: thesis: verumper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A39, XBOOLE_0:def 3;

end;

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, A37, A38, FUNCT_1:49

.= min (y1,jj) 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 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;mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, A37, A38, FUNCT_1:49

.= min (y1,jj) 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 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

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

then consider y2 being Real such that

A48: x2 = y2 and

A49: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, 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 Real : ( 0 <= x & x < 1 / 2 ) } by A46, A49;

hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

end;A48: x2 = y2 and

A49: ( 0 <= y2 & y2 < 1 / 2 ) ;

reconsider y2 = y2 as Real ;

mi . x9 = Mi . [x1,x2] by A37, A38, FUNCT_1:49

.= minreal . (x1,x2) by A19, 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 Real : ( 0 <= x & x < 1 / 2 ) } by A46, A49;

hence mi . x9 in B by A8, XBOOLE_0:def 3; :: thesis: verum

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 :: thesis: for a, b being Element of L9 holds

( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )

( 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

.= (maxreal || A) . [a,b] by FUNCT_1:49

.= maxreal . (a,b) by A19, 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, FUNCT_1:49 ; :: thesis: verum

end;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, 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, FUNCT_1:49 ; :: thesis: verum

A51: now :: thesis: for x1 being Element of B holds x1 is Element of L

let x1 be Element of B; :: thesis: b_{1} is Element of L

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

end;

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

then consider y being Real such that

A52: ( x1 = y & 0 <= y ) and

A53: y < 1 / 2 ;

y + (1 / 2) <= (1 / 2) + 1 by A53, XREAL_1:7;

then y <= 1 by XREAL_1:6;

then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A52;

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

end;A52: ( x1 = y & 0 <= y ) and

A53: y < 1 / 2 ;

y + (1 / 2) <= (1 / 2) + 1 by A53, XREAL_1:7;

then y <= 1 by XREAL_1:6;

then x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A52;

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

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

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;reconsider p9 = p, q9 = q as Element of L by A51;

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

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

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;reconsider p9 = p, q9 = q as Element of L by A51;

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

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

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;reconsider p9 = p, q9 = q as Element of L by A51;

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

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

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;reconsider p9 = p, q9 = q as Element of L by A51;

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

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

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;reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;

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

now :: thesis: for p, q, r being Element of L9 holds p "\/" (q "\/" r) = (p "\/" q) "\/" r

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 A54, A57, A56, A58, A55, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;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 A51;

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;reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;

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

then reconsider L9 = L9 as Lattice ;

reconsider L9 = L9 as SubLattice of RealSubLatt ((In (0,REAL)),(In (1,REAL))) by A13, A12, A11, A18, NAT_LAT:def 12;

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

hence
L9 is /\-inheriting
; :: thesis: not L9 is \/-inheriting let X be Subset of L9; :: thesis: "/\" (X,L) in the carrier of L9

thus "/\" (X,L) in the carrier of L9 :: thesis: verum

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

A59: "/\" (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 Real such that

A60: y = "/\" (X,L) and

A61: 0 <= y and

y <= 1 ;

reconsider y = y as Real ;

assume A62: not "/\" (X,L) in the carrier of L9 ; :: thesis: contradiction

then not "/\" (X,L) in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A8, XBOOLE_0:def 3;

then A63: 1 / 2 <= y by A60, A61;

end;then reconsider w = 1 as Element of L by A13, RCOMP_1:def 1;

A59: "/\" (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 Real such that

A60: y = "/\" (X,L) and

A61: 0 <= y and

y <= 1 ;

reconsider y = y as Real ;

assume A62: not "/\" (X,L) in the carrier of L9 ; :: thesis: contradiction

then not "/\" (X,L) in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } by A8, XBOOLE_0:def 3;

then A63: 1 / 2 <= y by A60, A61;

now :: thesis: for z9 being object st z9 in X holds

z9 in {1}

then A66:
X c= {1}
;z9 in {1}

let z9 be object ; :: thesis: ( z9 in X implies z9 in {1} )

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

A65: "/\" (X,L) [= z by A59, A64;

reconsider z1 = z as Real ;

reconsider z1 = z1 as Real ;

min (z1,y) = minreal . (z1,("/\" (X,L))) by A60, 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 A60, A65, LATTICES:4 ;

then y <= z1 by XXREAL_0:def 9;

then y + (1 / 2) <= z1 + y by A63, XREAL_1:7;

then for v being 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 Real : ( 0 <= x & x < 1 / 2 ) } ;

hence z9 in {1} by A8, XBOOLE_0:def 3; :: thesis: verum

end;assume A64: 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;

A65: "/\" (X,L) [= z by A59, A64;

reconsider z1 = z as Real ;

reconsider z1 = z1 as Real ;

min (z1,y) = minreal . (z1,("/\" (X,L))) by A60, 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 A60, A65, LATTICES:4 ;

then y <= z1 by XXREAL_0:def 9;

then y + (1 / 2) <= z1 + y by A63, XREAL_1:7;

then for v being 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 Real : ( 0 <= x & x < 1 / 2 ) } ;

hence z9 in {1} by A8, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( X = {} or X = {1} )
by A66, ZFMISC_1:33;

end;

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

w [= q by A67;

then w is_less_than X ;

then "/\" (X,L) = w by A68, LATTICE3:34;

then "/\" (X,L) in {1} by TARSKI:def 1;

hence contradiction by A8, A62, XBOOLE_0:def 3; :: thesis: verum

end;

A68: now :: thesis: for r1 being Element of L st r1 is_less_than X holds

r1 [= w

for q being Element of L st q in X holds r1 [= w

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 Real such that

A69: r1 = e and

0 <= e and

A70: e <= 1 ;

reconsider e = e as Real ;

r1 "/\" w = (minreal || A) . (r1,w) by A11, LATTICES:def 2

.= minreal . [r1,w] by A13, FUNCT_1:49

.= minreal . (r1,w)

.= min (e,jj) by A69, REAL_LAT:def 1

.= r1 by A69, A70, XXREAL_0:def 9 ;

hence r1 [= w by LATTICES:4; :: thesis: verum

end;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 Real such that

A69: r1 = e and

0 <= e and

A70: e <= 1 ;

reconsider e = e as Real ;

r1 "/\" w = (minreal || A) . (r1,w) by A11, LATTICES:def 2

.= minreal . [r1,w] by A13, FUNCT_1:49

.= minreal . (r1,w)

.= min (e,jj) by A69, REAL_LAT:def 1

.= r1 by A69, A70, XXREAL_0:def 9 ;

hence r1 [= w by LATTICES:4; :: thesis: verum

w [= q by A67;

then w is_less_than X ;

then "/\" (X,L) = w by A68, LATTICE3:34;

then "/\" (X,L) in {1} by TARSKI:def 1;

hence contradiction by A8, A62, XBOOLE_0:def 3; :: thesis: verum

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, A62, XBOOLE_0:def 3; :: thesis: verum

end;then "/\" (X,L) in {1} by TARSKI:def 1;

hence contradiction by A8, A62, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: not for X being Subset of L9 holds "\/" (X,L) in the carrier of L9

hence
not L9 is \/-inheriting
; :: thesis: verum
1 / 2 in { x where x is 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 Real : ( 0 <= x & x < 1 / 2 ) } ;

for y being Real holds

( not y = 1 / 2 or not 0 <= y or not y < 1 / 2 ) ;

then A71: ( not 1 / 2 in {1} & not 1 / 2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;

for x1 being object st x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } holds

x1 in B by A8, XBOOLE_0:def 3;

then reconsider X = { x where x is 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

then "\/" (X,L) = 1 / 2 by A72, LATTICE3:def 21;

hence not "\/" (X,L) in the carrier of L9 by A1, A71, XBOOLE_0:def 3; :: thesis: verum

end;then reconsider z = 1 / 2 as Element of L by A13, RCOMP_1:def 1;

set X = { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ;

for y being Real holds

( not y = 1 / 2 or not 0 <= y or not y < 1 / 2 ) ;

then A71: ( not 1 / 2 in {1} & not 1 / 2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } ) by TARSKI:def 1;

for x1 being object st x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } holds

x1 in B by A8, XBOOLE_0:def 3;

then reconsider X = { x where x is 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

A72: now :: thesis: for b being Element of L st X is_less_than b holds

z [= b

z [= b

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 Real such that

A73: b = b9 and

A74: 0 <= b9 and

A75: b9 <= 1 ;

reconsider b9 = b9 as Real ;

assume A76: X is_less_than b ; :: thesis: z [= b

A77: 1 / 2 <= b9

.= minreal . [z,b] by A13, FUNCT_1:49

.= minreal . (z,b)

.= min (jd,b9) by A73, REAL_LAT:def 1

.= z by A77, XXREAL_0:def 9 ;

hence z [= b by LATTICES:4; :: thesis: verum

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

A73: b = b9 and

A74: 0 <= b9 and

A75: b9 <= 1 ;

reconsider b9 = b9 as Real ;

assume A76: X is_less_than b ; :: thesis: z [= b

A77: 1 / 2 <= b9

proof

z "/\" b =
(minreal || A) . (z,b)
by A11, LATTICES:def 2
(1 / 2) + b9 <= 1 + 1
by A75, 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 A74;

then reconsider c = ((1 / 2) + b9) / 2 as Element of L by A13, RCOMP_1:def 1;

reconsider cc = c as Real ;

assume A78: b9 < 1 / 2 ; :: thesis: contradiction

then b9 + b9 < (1 / 2) + b9 by XREAL_1:6;

then A79: (b9 + b9) / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;

b9 + (1 / 2) < (1 / 2) + (1 / 2) by A78, XREAL_1:6;

then ((1 / 2) + b9) / 2 < 1 / 2 by XREAL_1:74;

then A80: (jd + b9) / 2 in X by A74;

b9 in X by A74, A78;

then b = "\/" (X,L) by A73, A76, LATTICE3:40;

then c [= b by A80, 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 . (cc,b)

.= min ((((1 / 2) + b9) / 2),b9) by A73, REAL_LAT:def 1 ;

hence contradiction by A79, XXREAL_0:def 9; :: thesis: verum

end;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 A74;

then reconsider c = ((1 / 2) + b9) / 2 as Element of L by A13, RCOMP_1:def 1;

reconsider cc = c as Real ;

assume A78: b9 < 1 / 2 ; :: thesis: contradiction

then b9 + b9 < (1 / 2) + b9 by XREAL_1:6;

then A79: (b9 + b9) / 2 < ((1 / 2) + b9) / 2 by XREAL_1:74;

b9 + (1 / 2) < (1 / 2) + (1 / 2) by A78, XREAL_1:6;

then ((1 / 2) + b9) / 2 < 1 / 2 by XREAL_1:74;

then A80: (jd + b9) / 2 in X by A74;

b9 in X by A74, A78;

then b = "\/" (X,L) by A73, A76, LATTICE3:40;

then c [= b by A80, 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 . (cc,b)

.= min ((((1 / 2) + b9) / 2),b9) by A73, REAL_LAT:def 1 ;

hence contradiction by A79, XXREAL_0:def 9; :: thesis: verum

.= minreal . [z,b] by A13, FUNCT_1:49

.= minreal . (z,b)

.= min (jd,b9) by A73, REAL_LAT:def 1

.= z by A77, XXREAL_0:def 9 ;

hence z [= b by LATTICES:4; :: thesis: verum

now :: thesis: for q being Element of L st q in X holds

q [= z

then
X is_less_than z
;q [= z

let q be Element of L; :: thesis: ( q in X implies q [= z )

assume q in X ; :: thesis: q [= z

then A81: ex y being 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 Real such that

A82: q = q9 and

0 <= q9 and

q9 <= 1 ;

reconsider q9 = q9 as Real ;

q "/\" z = (minreal || A) . (q,z) by A11, LATTICES:def 2

.= minreal . [q,z] by A13, FUNCT_1:49

.= minreal . (q,z)

.= min (q9,jd) by A82, REAL_LAT:def 1

.= q by A82, A81, XXREAL_0:def 9 ;

hence q [= z by LATTICES:4; :: thesis: verum

end;assume q in X ; :: thesis: q [= z

then A81: ex y being 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 Real such that

A82: q = q9 and

0 <= q9 and

q9 <= 1 ;

reconsider q9 = q9 as Real ;

q "/\" z = (minreal || A) . (q,z) by A11, LATTICES:def 2

.= minreal . [q,z] by A13, FUNCT_1:49

.= minreal . (q,z)

.= min (q9,jd) by A82, REAL_LAT:def 1

.= q by A82, A81, XXREAL_0:def 9 ;

hence q [= z by LATTICES:4; :: thesis: verum

then "\/" (X,L) = 1 / 2 by A72, LATTICE3:def 21;

hence not "\/" (X,L) in the carrier of L9 by A1, A71, XBOOLE_0:def 3; :: thesis: verum