set N = B_6 ;
set Z = {0,1,(3 \ 1),2,(3 \ 2),3};
A1:
the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
A2:
B_6 is with_suprema
proof
let x,
y be
Element of
B_6;
LATTICE3:def 10 ex b1 being Element of the carrier of B_6 st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of B_6 holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
A3:
{0,1,(3 \ 1),2,(3 \ 2),3} = the
carrier of
B_6
by YELLOW_1:1;
thus
ex
z being
Element of
B_6 st
(
x <= z &
y <= z & ( for
z9 being
Element of
B_6 st
x <= z9 &
y <= z9 holds
z <= z9 ) )
verumproof
per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) )
by A3, ENUMSET1:def 4;
suppose A4:
(
x = 3
\ 1 &
y = 2 )
;
ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
3
in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z = 3 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
Segm 2
c= Segm 3
by NAT_1:39;
hence
(
x <= z &
y <= z )
by A4, YELLOW_1:3;
for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9let z9 be
Element of
B_6;
( x <= z9 & y <= z9 implies z <= z9 )assume that A5:
x <= z9
and A6:
y <= z9
;
z <= z9A7:
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
A8:
3
\ 1
c= z9
by A4, A5, YELLOW_1:3;
A11:
Segm 2
c= z9
by A4, A6, YELLOW_1:3;
A12:
now not z9 = 3 \ 1end; A14:
now not z9 = 3 \ 2end;
( 1
in 2 &
0 in 2 )
by TARSKI:def 2, CARD_1:50;
then
( 1
in z9 &
0 in z9 )
by A11;
then
(
z9 <> 1 &
z9 <> 0 )
;
hence
z <= z9
by A7, A12, A9, A14, ENUMSET1:def 4;
verum end; suppose A18:
(
x = 1 &
y = 3
\ 2 )
;
ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
3
in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z = 3 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
Segm 1
c= Segm 3
by NAT_1:39;
hence
(
x <= z &
y <= z )
by A18, YELLOW_1:3;
for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9let z9 be
Element of
B_6;
( x <= z9 & y <= z9 implies z <= z9 )assume that A19:
x <= z9
and A20:
y <= z9
;
z <= z9A21:
3
\ 2
c= z9
by A18, A20, YELLOW_1:3;
A26:
1
c= z9
by A18, A19, YELLOW_1:3;
A27:
now not z9 = 3 \ 1end; A29:
now not z9 = 3 \ 2end;
(
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3} &
z9 <> 0 )
by A26, YELLOW_1:1;
hence
z <= z9
by A27, A24, A29, A22, ENUMSET1:def 4;
verum end; suppose A35:
(
y = 1 &
x = 3
\ 2 )
;
ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
3
in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z = 3 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
Segm 1
c= Segm 3
by NAT_1:39;
hence
(
x <= z &
y <= z )
by A35, YELLOW_1:3;
for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9let z9 be
Element of
B_6;
( x <= z9 & y <= z9 implies z <= z9 )assume that A36:
x <= z9
and A37:
y <= z9
;
z <= z9A38:
3
\ 2
c= z9
by A35, A36, YELLOW_1:3;
A43:
1
c= z9
by A35, A37, YELLOW_1:3;
A44:
now not z9 = 3 \ 1end; A46:
now not z9 = 3 \ 2end;
(
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3} &
z9 <> 0 )
by A43, YELLOW_1:1;
hence
z <= z9
by A44, A41, A46, A39, ENUMSET1:def 4;
verum end; suppose A50:
(
x = 2 &
y = 3
\ 1 )
;
ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
3
in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z = 3 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
Segm 2
c= Segm 3
by NAT_1:39;
hence
(
x <= z &
y <= z )
by A50, YELLOW_1:3;
for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9let z9 be
Element of
B_6;
( x <= z9 & y <= z9 implies z <= z9 )assume that A51:
x <= z9
and A52:
y <= z9
;
z <= z9A53:
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
A54:
3
\ 1
c= z9
by A50, A52, YELLOW_1:3;
A57:
2
c= z9
by A50, A51, YELLOW_1:3;
A58:
now not z9 = 3 \ 1end; A60:
now not z9 = 3 \ 2end;
( 1
in 2 &
0 in 2 )
by CARD_1:50, TARSKI:def 2;
then
( 1
in z9 &
0 in z9 )
by A57;
then
(
z9 <> 1 &
z9 <> 0 )
;
hence
z <= z9
by A53, A58, A55, A60, ENUMSET1:def 4;
verum end; end;
end;
end;
B_6 is with_infima
proof
let x,
y be
Element of
B_6;
LATTICE3:def 11 ex b1 being Element of the carrier of B_6 st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of B_6 holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
A68:
{0,1,(3 \ 1),2,(3 \ 2),3} = the
carrier of
B_6
by YELLOW_1:1;
thus
ex
z being
Element of
B_6 st
(
z <= x &
z <= y & ( for
z9 being
Element of
B_6 st
z9 <= x &
z9 <= y holds
z9 <= z ) )
verumproof
per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) )
by A68, ENUMSET1:def 4;
suppose A69:
(
x = 3
\ 1 &
y = 2 )
;
ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
0 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z =
0 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(
z c= x &
z c= y )
;
hence
(
z <= x &
z <= y )
by YELLOW_1:3;
for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= zlet z9 be
Element of
B_6;
( z9 <= x & z9 <= y implies z9 <= z )assume that A70:
z9 <= x
and A71:
z9 <= y
;
z9 <= zA72:
z9 c= 3
\ 1
by A69, A70, YELLOW_1:3;
A74:
z9 c= 2
by A69, A71, YELLOW_1:3;
A75:
now not z9 = 3 \ 1end; A79:
now not z9 = 3 \ 2end;
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
hence
z9 <= z
by A75, A73, A79, A81, A77, ENUMSET1:def 4;
verum end; suppose A85:
(
x = 2 &
y = 3
\ 1 )
;
ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
0 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;
then reconsider z =
0 as
Element of
B_6 by YELLOW_1:1;
take
z
;
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(
z c= x &
z c= y )
;
hence
(
z <= x &
z <= y )
by YELLOW_1:3;
for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= zlet z9 be
Element of
B_6;
( z9 <= x & z9 <= y implies z9 <= z )assume that A86:
z9 <= x
and A87:
z9 <= y
;
z9 <= zA88:
z9 c= 3
\ 1
by A85, A87, YELLOW_1:3;
A90:
z9 c= 2
by A85, A86, YELLOW_1:3;
A91:
now not z9 = 3 \ 1end; A95:
now not z9 = 3 \ 2end;
z9 is
Element of
{0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
hence
z9 <= z
by A91, A89, A95, A93, A97, ENUMSET1:def 4;
verum end; end;
end;
end;
hence
( B_6 is with_suprema & B_6 is with_infima )
by A2; verum