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; :: according to LATTICE3:def 10 :: thesis:
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 ) ) :: thesis:

proof

per cases by A3, ENUMSET1:def 4;

suppose ( x = 0 & y = 0 ) ; :: thesis:

then reconsider z = x \/ y as Element of B_6 ;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 0 & y = 3 \ 1 ) ; :: thesis:

end;

suppose ( x = 0 & y = 2 ) ; :: thesis:

end;

suppose ( x = 0 & y = 3 \ 2 ) ; :: thesis:

end;

suppose ( x = 0 & y = 3 ) ; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 0 ) ; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 3 \ 1 ) ; :: thesis:

end;

suppose A4: ( x = 3 \ 1 & y = 2 ) ; :: thesis:

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 ; :: thesis:
Segm 2 c= Segm 3 by NAT_1:39;
hence ( x <= z & y <= z ) by A4, YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A5: x <= z9 and
A6: y <= z9 ; :: thesis:
A7: 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;

A9: now :: thesis:

assume z9 = 2 ; :: thesis:
then A10: not 2 in z9 ;
2 in 3 \ 1 by TARSKI:def 2, YELLOW11:3;
hence contradiction by A8, A10; :: thesis:

end;

A11: Segm 2 c= z9 by A4, A6, YELLOW_1:3;

A12: now :: thesis:

A13: 0 in 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 1 ; :: thesis:
hence contradiction by A11, A13, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A14: now :: thesis:

A15: Segm 1 in Segm 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 2 ; :: thesis:
hence contradiction by A11, A15, TARSKI:def 1, YELLOW11:4; :: thesis:

end;

( 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; :: thesis:

end;

suppose ( x = 1 & y = 0 ) ; :: thesis:

end;

suppose ( x = 1 & y = 1 ) ; :: thesis:

end;

suppose A16: ( x = 1 & y = 3 \ 1 ) ; :: thesis:

A17: Segm 1 c= Segm 3 by NAT_1:39;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A17, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by A1, A16, ENUMSET1:def 4;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A18: ( x = 1 & y = 3 \ 2 ) ; :: thesis:

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 ; :: thesis:
Segm 1 c= Segm 3 by NAT_1:39;
hence ( x <= z & y <= z ) by A18, YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A19: x <= z9 and
A20: y <= z9 ; :: thesis:
A21: 3 \ 2 c= z9 by A18, A20, YELLOW_1:3;

A22: now :: thesis:

A23: 2 in 3 \ 2 by TARSKI:def 1, YELLOW11:4;
assume z9 = 1 ; :: thesis:
hence contradiction by A21, A23, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A24: now :: thesis:

assume z9 = 2 ; :: thesis:
then A25: not 2 in z9 ;
2 in 3 \ 2 by TARSKI:def 1, YELLOW11:4;
hence contradiction by A21, A25; :: thesis:

end;

A26: 1 c= z9 by A18, A19, YELLOW_1:3;

A27: now :: thesis:

A28: 0 in 1 by CARD_1:49, TARSKI:def 1;
assume z9 = 3 \ 1 ; :: thesis:
hence contradiction by A26, A28, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A29: now :: thesis:

A30: 0 in 1 by CARD_1:49, TARSKI:def 1;
assume z9 = 3 \ 2 ; :: thesis:
hence contradiction by A26, A30, TARSKI:def 1, YELLOW11:4; :: thesis:

end;

( 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; :: thesis:

end;

suppose A31: ( x = 1 & y = 3 ) ; :: thesis:

Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A31, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A32: ( x = 1 & y = 2 ) ; :: thesis:

Segm 1 c= Segm 2 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A32, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( y = 1 & x = 0 ) ; :: thesis:

end;

suppose ( y = 1 & x = 1 ) ; :: thesis:

end;

suppose A33: ( y = 1 & x = 3 \ 1 ) ; :: thesis:

A34: Segm 1 c= Segm 3 by NAT_1:39;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A34, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by A1, A33, ENUMSET1:def 4;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A35: ( y = 1 & x = 3 \ 2 ) ; :: thesis:

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 ; :: thesis:
Segm 1 c= Segm 3 by NAT_1:39;
hence ( x <= z & y <= z ) by A35, YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A36: x <= z9 and
A37: y <= z9 ; :: thesis:
A38: 3 \ 2 c= z9 by A35, A36, YELLOW_1:3;

A39: now :: thesis:

A40: 2 in 3 \ 2 by TARSKI:def 1, YELLOW11:4;
assume z9 = 1 ; :: thesis:
hence contradiction by A38, A40, CARD_1:49, TARSKI:def 1; :: thesis:

end;

A41: now :: thesis:

assume z9 = 2 ; :: thesis:
then A42: not 2 in z9 ;
2 in 3 \ 2 by TARSKI:def 1, YELLOW11:4;
hence contradiction by A38, A42; :: thesis:

end;

A43: 1 c= z9 by A35, A37, YELLOW_1:3;

A44: now :: thesis:

A45: 0 in 1 by CARD_1:49, TARSKI:def 1;
assume z9 = 3 \ 1 ; :: thesis:
hence contradiction by A43, A45, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A46: now :: thesis:

A47: 0 in 1 by CARD_1:49, TARSKI:def 1;
assume z9 = 3 \ 2 ; :: thesis:
hence contradiction by A43, A47, TARSKI:def 1, YELLOW11:4; :: thesis:

end;

( 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; :: thesis:

end;

suppose A48: ( y = 1 & x = 3 ) ; :: thesis:

Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A48, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A49: ( y = 1 & x = 2 ) ; :: thesis:

Segm 1 c= Segm 2 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A49, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 3 \ 2 ) ; :: thesis:

then reconsider z = x \/ y as Element of B_6 by Lm2, XBOOLE_1:12, XBOOLE_1:34;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 3 ) ; :: thesis:

then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 2 & y = 0 ) ; :: thesis:

end;

suppose A50: ( x = 2 & y = 3 \ 1 ) ; :: thesis:

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 ; :: thesis:
Segm 2 c= Segm 3 by NAT_1:39;
hence ( x <= z & y <= z ) by A50, YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A51: x <= z9 and
A52: y <= z9 ; :: thesis:
A53: 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;

A55: now :: thesis:

assume z9 = 2 ; :: thesis:
then A56: not 2 in z9 ;
2 in 3 \ 1 by TARSKI:def 2, YELLOW11:3;
hence contradiction by A54, A56; :: thesis:

end;

A57: 2 c= z9 by A50, A51, YELLOW_1:3;

A58: now :: thesis:

A59: 0 in 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 1 ; :: thesis:
hence contradiction by A57, A59, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A60: now :: thesis:

A61: 1 in 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 2 ; :: thesis:
hence contradiction by A57, A61, TARSKI:def 1, YELLOW11:4; :: thesis:

end;

( 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; :: thesis:

end;

suppose ( x = 2 & y = 2 ) ; :: thesis:

end;

suppose A62: ( x = 2 & y = 3 \ 2 ) ; :: thesis:

A63: Segm 2 c= Segm 3 by NAT_1:39;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A63, XBOOLE_1:12 ;
then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A62, ENUMSET1:def 4;
then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A64: ( x = 2 & y = 3 ) ; :: thesis:

Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A64, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 0 ) ; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 3 \ 1 ) ; :: thesis:

end;

suppose A65: ( x = 3 \ 2 & y = 2 ) ; :: thesis:

A66: Segm 2 c= Segm 3 by NAT_1:39;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A66, XBOOLE_1:12 ;
then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A65, ENUMSET1:def 4;
then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 3 \ 2 ) ; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 3 ) ; :: thesis:

end;

suppose ( x = 3 & y = 0 ) ; :: thesis:

end;

suppose ( x = 3 & y = 3 \ 1 ) ; :: thesis:

end;

suppose A67: ( x = 3 & y = 2 ) ; :: thesis:

Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A67, XBOOLE_1:12;
take z ; :: thesis:
( x c= z & y c= z ) by XBOOLE_1:7;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( x <= w & y <= w ) ; :: thesis:
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 & y = 3 \ 2 ) ; :: thesis:

end;

suppose ( x = 3 & y = 3 ) ; :: thesis:

end;

B_6 is with_infima

proof

let x, y be Element of B_6; :: according to LATTICE3:def 11 :: thesis:
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 ) ) :: thesis:

proof

per cases by A68, ENUMSET1:def 4;

suppose ( x = 0 & y = 0 ) ; :: thesis:

then reconsider z = x /\ y as Element of B_6 ;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 0 & y = 3 \ 1 ) ; :: thesis:

end;

suppose ( x = 0 & y = 2 ) ; :: thesis:

end;

suppose ( x = 0 & y = 3 \ 2 ) ; :: thesis:

end;

suppose ( x = 0 & y = 3 ) ; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 0 ) ; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 3 \ 1 ) ; :: thesis:

end;

suppose A69: ( x = 3 \ 1 & y = 2 ) ; :: thesis:

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 ; :: thesis:
( z c= x & z c= y ) ;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A70: z9 <= x and
A71: z9 <= y ; :: thesis:
A72: z9 c= 3 \ 1 by A69, A70, YELLOW_1:3;

A73: now :: thesis:

assume z9 = 2 ; :: thesis:
then 0 in z9 by CARD_1:50, TARSKI:def 2;
hence contradiction by A72, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A74: z9 c= 2 by A69, A71, YELLOW_1:3;

A75: now :: thesis:

assume z9 = 3 \ 1 ; :: thesis:
then A76: 2 in z9 by TARSKI:def 2, YELLOW11:3;
not 2 in 2 ;
hence contradiction by A74, A76; :: thesis:

end;

A77: now :: thesis:

assume z9 = 3 ; :: thesis:
then A78: 2 in z9 by CARD_1:51, ENUMSET1:def 1;
not 2 in 2 ;
hence contradiction by A74, A78; :: thesis:

end;

A79: now :: thesis:

assume z9 = 3 \ 2 ; :: thesis:
then A80: 2 in z9 by TARSKI:def 1, YELLOW11:4;
not 2 in 2 ;
hence contradiction by A74, A80; :: thesis:

end;

A81: now :: thesis:

assume z9 = 1 ; :: thesis:
then 0 in z9 by CARD_1:49, TARSKI:def 1;
hence contradiction by A72, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

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; :: thesis:

end;

suppose ( x = 1 & y = 0 ) ; :: thesis:

end;

suppose ( x = 1 & y = 1 ) ; :: thesis:

end;

suppose ( x = 1 & y = 3 \ 1 ) ; :: thesis:

then x misses y by XBOOLE_1:79;
then x /\ y = 0 by XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 1 & y = 3 \ 2 ) ; :: thesis:

then x /\ y = 0 by Lm3, XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A82: ( x = 1 & y = 3 ) ; :: thesis:

Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A82, XBOOLE_1:28;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 1 & y = 2 ) ; :: thesis:

then reconsider z = x /\ y as Element of B_6 by CARD_1:49, CARD_1:50, ZFMISC_1:13;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( y = 1 & x = 0 ) ; :: thesis:

end;

suppose ( y = 1 & x = 1 ) ; :: thesis:

end;

suppose ( y = 1 & x = 3 \ 1 ) ; :: thesis:

end;

suppose ( y = 1 & x = 3 \ 2 ) ; :: thesis:

then x /\ y = {} by Lm3, XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A83: ( y = 1 & x = 3 ) ; :: thesis:

Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A83, XBOOLE_1:28;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( y = 1 & x = 2 ) ; :: thesis:

end;

suppose ( x = 3 \ 1 & y = 3 \ 2 ) ; :: thesis:

then reconsider z = x /\ y as Element of B_6 by YELLOW11:3, YELLOW11:4, ZFMISC_1:13;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A84: ( x = 3 \ 1 & y = 3 ) ; :: thesis:

(3 \ 1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3 \ 1 ;
then reconsider z = x /\ y as Element of B_6 by A84;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 2 & y = 0 ) ; :: thesis:

end;

suppose A85: ( x = 2 & y = 3 \ 1 ) ; :: thesis:

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 ; :: thesis:
( z c= x & z c= y ) ;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let z9 be Element of B_6; :: thesis:
assume that
A86: z9 <= x and
A87: z9 <= y ; :: thesis:
A88: z9 c= 3 \ 1 by A85, A87, YELLOW_1:3;

A89: now :: thesis:

assume z9 = 2 ; :: thesis:
then 0 in z9 by CARD_1:50, TARSKI:def 2;
hence contradiction by A88, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

A90: z9 c= 2 by A85, A86, YELLOW_1:3;

A91: now :: thesis:

assume z9 = 3 \ 1 ; :: thesis:
then A92: 2 in z9 by TARSKI:def 2, YELLOW11:3;
not 2 in 2 ;
hence contradiction by A90, A92; :: thesis:

end;

A93: now :: thesis:

assume z9 = 3 ; :: thesis:
then A94: 2 in z9 by CARD_1:51, ENUMSET1:def 1;
not 2 in 2 ;
hence contradiction by A90, A94; :: thesis:

end;

A95: now :: thesis:

assume z9 = 3 \ 2 ; :: thesis:
then A96: 2 in z9 by TARSKI:def 1, YELLOW11:4;
not 2 in 2 ;
hence contradiction by A90, A96; :: thesis:

end;

A97: now :: thesis:

assume z9 = 1 ; :: thesis:
then 0 in z9 by CARD_1:49, TARSKI:def 1;
hence contradiction by A88, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

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; :: thesis:

end;

suppose ( x = 2 & y = 2 ) ; :: thesis:

end;

suppose A98: ( x = 2 & y = 3 \ 2 ) ; :: thesis:

2 misses 3 \ 2 by XBOOLE_1:79;
then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;
then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A98, ENUMSET1:def 4;
then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A99: ( x = 2 & y = 3 ) ; :: thesis:

Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A99, XBOOLE_1:28;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 0 ) ; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 3 \ 1 ) ; :: thesis:

end;

suppose A100: ( x = 3 \ 2 & y = 2 ) ; :: thesis:

2 misses 3 \ 2 by XBOOLE_1:79;
then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;
then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A100, ENUMSET1:def 4;
then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 \ 2 & y = 3 \ 2 ) ; :: thesis:

end;

suppose A101: ( x = 3 \ 2 & y = 3 ) ; :: thesis:

(3 \ 2) /\ 3 = (3 /\ 3) \ 2 by XBOOLE_1:49
.= 3 \ 2 ;
then reconsider z = x /\ y as Element of B_6 by A101;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 & y = 0 ) ; :: thesis:

end;

suppose A102: ( x = 3 & y = 3 \ 1 ) ; :: thesis:

(3 \ 1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3 \ 1 ;
then reconsider z = x /\ y as Element of B_6 by A102;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A103: ( x = 3 & y = 2 ) ; :: thesis:

Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A103, XBOOLE_1:28;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A104: ( x = 3 & y = 3 \ 2 ) ; :: thesis:

(3 \ 2) /\ 3 = (3 /\ 3) \ 2 by XBOOLE_1:49
.= 3 \ 2 ;
then reconsider z = x /\ y as Element of B_6 by A104;
take z ; :: thesis:
( z c= x & z c= y ) by XBOOLE_1:17;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis:
let w be Element of B_6; :: thesis:
assume ( w <= x & w <= y ) ; :: thesis:
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose ( x = 3 & y = 3 ) ; :: thesis:

end;

hence ( B_6 is with_suprema & B_6 is with_infima ) by A2; :: thesis: