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 z' being Element of B_6 st x <= z' & y <= z' holds
z <= z' ) ) :: 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:
y c= z by A4, NAT_1:40;
hence ( x <= z & y <= z ) by A4, YELLOW_1:3; :: thesis:
let z' be Element of B_6 ; :: thesis:
assume that
A5: x <= z' and
A6: y <= z' ; :: thesis:
A7: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A8: 3 \ 1 c= z' by A4, A5, YELLOW_1:3;

A9: now

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

end;

A11: 2 c= z' by A4, A6, YELLOW_1:3;

A12: now

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

end;

A14: now

A15: 1 in 2 by CARD_1:88, TARSKI:def 2;
assume z' = 3 \ 2 ; :: thesis:
hence contradiction by A11, A15, TARSKI:def 1, YELLOW11:4; :: thesis:

end;

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

A22: now

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

end;

A24: now

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

end;

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

A27: now

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

end;

A29: now

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

end;

( z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} & z' <> 0 ) by A26, YELLOW_1:1;
hence z <= z' by A27, A24, A29, A22, ENUMSET1:def 4; :: thesis:

end;

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

1 c= 3 by NAT_1:40;
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:

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

A39: now

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

end;

A41: now

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

end;

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

A44: now

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

end;

A46: now

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

end;

( z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} & z' <> 0 ) by A43, YELLOW_1:1;
hence z <= z' by A44, A41, A46, A39, ENUMSET1:def 4; :: thesis:

end;

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

1 c= 3 by NAT_1:40;
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:

1 c= 2 by NAT_1:40;
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:
x c= z by A50, NAT_1:40;
hence ( x <= z & y <= z ) by A50, YELLOW_1:3; :: thesis:
let z' be Element of B_6 ; :: thesis:
assume that
A51: x <= z' and
A52: y <= z' ; :: thesis:
A53: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A54: 3 \ 1 c= z' by A50, A52, YELLOW_1:3;

A55: now

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

end;

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

A58: now

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

end;

A60: now

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

end;

( z' <> 1 & z' <> 0 ) by A57, NAT_1:40;
hence z <= z' 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: 2 c= 3 by NAT_1:40;
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:

2 c= 3 by NAT_1:40;
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: 2 c= 3 by NAT_1:40;
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:

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

A73: now

assume z' = 2 ; :: thesis:
then 0 in z' by CARD_1:88, TARSKI:def 2;
hence contradiction by A72, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

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

A75: now

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

end;

A77: now

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

end;

A79: now

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

end;

A81: now

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

end;

z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence z' <= 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:

1 c= 3 by NAT_1:40;
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:87, CARD_1:88, ZFMISC_1:19;
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:

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

A89: now

assume z' = 2 ; :: thesis:
then 0 in z' by CARD_1:88, TARSKI:def 2;
hence contradiction by A88, TARSKI:def 2, YELLOW11:3; :: thesis:

end;

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

A91: now

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

end;

A93: now

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

end;

A95: now

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

end;

A97: now

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

end;

z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence z' <= 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:

2 c= 3 by NAT_1:40;
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:

2 c= 3 by NAT_1:40;
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: