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 ) }
{1} \/ { x where x is Real : ( 0 <= x & x < 1 / 2 ) } c= {0,1} \/ ].0,(1 / 2).[
then A8:
{0,1} \/ ].0,(1 / 2).[ = {1} \/ { x where x is 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:
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 for x1 being object st x1 in B holds
x1 in Alet x1 be
object ;
( x1 in B implies x1 in A )assume A15:
x1 in B
;
x1 in Ahence
x1 in A
;
verum end;
then A18:
B c= A
;
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 for x9 being object st x9 in dom ma holds
ma . x9 in Blet x9 be
object ;
( x9 in dom ma implies ma . x9 in B )assume A22:
x9 in dom ma
;
ma . x9 in Bthen 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 ma . x9 in Bper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A25, XBOOLE_0:def 3;
suppose
x1 in {1}
;
ma . x9 in Bthen A26:
x1 = 1
by TARSKI:def 1;
now ma . x9 in Bper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A24, XBOOLE_0:def 3;
suppose
x2 in {1}
;
ma . x9 in Bthen 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;
verum end; suppose
x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
ma . x9 in Bthen 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;
verum end; end; end; hence
ma . x9 in B
;
verum end; suppose
x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
ma . x9 in Bthen consider y1 being
Real such that A30:
x1 = y1
and A31:
(
0 <= y1 &
y1 < 1
/ 2 )
;
reconsider y1 =
y1 as
Real ;
now ma . x9 in Bper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A24, XBOOLE_0:def 3;
suppose
x2 in {1}
;
ma . x9 in Bthen 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;
verum end; suppose
x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
ma . x9 in Bthen 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;
verum end; end; end; hence
ma . x9 in B
;
verum end; end; end; hence
ma . x9 in B
;
verum end;
A35:
dom mi = [:B,B:]
by FUNCT_2:def 1;
A36:
now for x9 being object st x9 in dom mi holds
mi . x9 in Blet x9 be
object ;
( x9 in dom mi implies mi . x9 in B )assume A37:
x9 in dom mi
;
mi . x9 in Bthen 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 mi . x9 in Bper cases
( x1 in {1} or x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A40, XBOOLE_0:def 3;
suppose
x1 in {1}
;
mi . x9 in Bthen A41:
x1 = 1
by TARSKI:def 1;
now mi . x9 in Bper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A39, XBOOLE_0:def 3;
suppose
x2 in {1}
;
mi . x9 in Bthen 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;
verum end; suppose
x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
mi . x9 in Bthen 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;
verum end; end; end; hence
mi . x9 in B
;
verum end; suppose
x1 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
mi . x9 in Bthen consider y1 being
Real such that A45:
x1 = y1
and A46:
(
0 <= y1 &
y1 < 1
/ 2 )
;
reconsider y1 =
y1 as
Real ;
now mi . x9 in Bper cases
( x2 in {1} or x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) } )
by A1, A39, XBOOLE_0:def 3;
suppose
x2 in {1}
;
mi . x9 in Bthen 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;
verum end; suppose
x2 in { x where x is Real : ( 0 <= x & x < 1 / 2 ) }
;
mi . x9 in Bthen 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;
verum end; end; end; hence
mi . x9 in B
;
verum end; end; end; hence
mi . x9 in B
;
verum end;
reconsider L = RealSubLatt ((In (0,REAL)),(In (1,REAL))) as complete Lattice by Th20;
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 for a, b being Element of L9 holds
( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )let a,
b be
Element of
L9;
( 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
;
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
;
verum end;
A58:
now for p, q, r being Element of L9 holds p "/\" (q "/\" r) = (p "/\" q) "/\" rlet p,
q,
r be
Element of
L9;
p "/\" (q "/\" r) = (p "/\" q) "/\" rreconsider 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
;
verum end;
now for p, q, r being Element of L9 holds p "\/" (q "\/" r) = (p "\/" q) "\/" rlet p,
q,
r be
Element of
L9;
p "\/" (q "\/" r) = (p "\/" q) "\/" rreconsider 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
;
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 A54, A57, A56, A58, A55, 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 ((In (0,REAL)),(In (1,REAL))) by A13, A12, A11, A18, NAT_LAT:def 12;
take
L9
; ( L9 is /\-inheriting & not L9 is \/-inheriting )
now for X being Subset of L9 holds "/\" (X,L) in the carrier of L9let X be
Subset of
L9;
"/\" (X,L) in the carrier of L9thus
"/\" (
X,
L)
in the
carrier of
L9
verumproof
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
;
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 for z9 being object st z9 in X holds
z9 in {1}let z9 be
object ;
( z9 in X implies z9 in {1} )assume A64:
z9 in X
;
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;
verum end;
then A66:
X c= {1}
;
now contradictionper cases
( X = {} or X = {1} )
by A66, ZFMISC_1:33;
suppose A67:
X = {}
;
contradictionA68:
now for r1 being Element of L st r1 is_less_than X holds
r1 [= wlet r1 be
Element of
L;
( r1 is_less_than X implies r1 [= w )assume
r1 is_less_than X
;
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;
verum end;
for
q being
Element of
L st
q in X holds
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;
verum end; end; end;
hence
contradiction
;
verum
end; end;
hence
L9 is /\-inheriting
; not L9 is \/-inheriting
now not for X being Subset of L9 holds "\/" (X,L) in the carrier of L9
1
/ 2
in { x where x is Real : ( 0 <= x & x <= 1 ) }
;
then reconsider z = 1
/ 2 as
Element of
L by 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;
not "\/" (X,L) in the carrier of L9A72:
now for b being Element of L st X is_less_than b holds
z [= blet b be
Element of
L;
( 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
;
z [= bA77:
1
/ 2
<= b9
proof
(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
;
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;
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 (
jd,
b9)
by A73, REAL_LAT:def 1
.=
z
by A77, XXREAL_0:def 9
;
hence
z [= b
by LATTICES:4;
verum end; then
X is_less_than z
;
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;
verum end;
hence
not L9 is \/-inheriting
; verum