set Z = {0 ,1,(3 \ 1),2,(3 \ 2),3};
set N = B_6 ;
AA: the carrier of B_6 = {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A1: B_6 is with_suprema

proof

let x, y be Element of B_6 ; :: according to LATTICE3:def 10 :: thesis:
A8: {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 A8, 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 A9: ( 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:
( x c= z & y c= z ) by A9, NAT_1:40;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of B_6 ; :: thesis:
A10: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A11: ( 3 \ 1 c= z' & 2 c= z' ) by A9, YELLOW_1:3;

A12: now

assume z' = 3 \ 1 ; :: thesis:
then ( not 0 in z' & 0 in 2 ) by CARD_1:88, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A13: now

assume z' = 2 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 1 ) by TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( not 1 in z' & 1 in 2 ) by CARD_1:88, TARSKI:def 1, TARSKI:def 2, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A00: z' <> 1 by A11, NAT_1:40;
z' <> 0 by A11;
hence z <= z' by A00, A10, A12, A13, A14, ENUMSET1:def 4; :: thesis:

end;

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

end;

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

end;

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

B: 1 c= 3 by NAT_1:40;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by B, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by AA, A, 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 A9: ( x = 1 & y = 3 \ 2 ) ; :: thesis:

A12: now

assume z' = 3 \ 1 ; :: thesis:
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A13: now

assume z' = 2 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 2 ) by TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A00: now

assume z' = 1 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 2 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

z' <> 0 by A11;
hence z <= z' by A00, A10, A12, A13, A14, ENUMSET1:def 4; :: thesis:

end;

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

1 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of B_6 by F1, 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 AA: ( x = 1 & y = 2 ) ; :: thesis:

1 c= 2 by NAT_1:40;
then reconsider z = x \/ y as Element of B_6 by AA, 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 A: ( y = 1 & x = 3 \ 1 ) ; :: thesis:

B: 1 c= 3 by NAT_1:40;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by B, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by A, AA, 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 A9: ( y = 1 & x = 3 \ 2 ) ; :: thesis:

A12: now

assume z' = 3 \ 1 ; :: thesis:
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A13: now

assume z' = 2 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 2 ) by TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A00: now

assume z' = 1 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 2 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

z' <> 0 by A11;
hence z <= z' by A00, A10, A12, A13, A14, ENUMSET1:def 4; :: thesis:

end;

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

end;

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

1 c= 2 by NAT_1:40;
then reconsider z = x \/ y as Element of B_6 by F1, 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 L2, 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 A16: ( 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 & y c= z ) by A16, NAT_1:40;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of B_6 ; :: thesis:
A10: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A11: ( 3 \ 1 c= z' & 2 c= z' ) by A16, YELLOW_1:3;

A12: now

assume z' = 3 \ 1 ; :: thesis:
then ( not 0 in z' & 0 in 2 ) by CARD_1:88, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A13: now

assume z' = 2 ; :: thesis:
then ( not 2 in z' & 2 in 3 \ 1 ) by TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( not 1 in z' & 1 in 2 ) by CARD_1:88, TARSKI:def 1, TARSKI:def 2, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A00: z' <> 1 by A11, NAT_1:40;
z' <> 0 by A11;
hence z <= z' by A00, A10, A12, A13, A14, ENUMSET1:def 4; :: thesis:

end;

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

end;

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

A: 2 c= 3 by NAT_1:40;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A, XBOOLE_1:12 ;
then x \/ y in {0 ,1,(3 \ 1),2,(3 \ 2),3} by A22, 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 A23: ( x = 2 & y = 3 ) ; :: thesis:

2 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of B_6 by A23, 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 A24: ( x = 3 \ 2 & y = 2 ) ; :: thesis:

A: 2 c= 3 by NAT_1:40;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A, XBOOLE_1:12 ;
then x \/ y in {0 ,1,(3 \ 1),2,(3 \ 2),3} by A24, 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 A27: ( x = 3 & y = 2 ) ; :: thesis:

2 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of B_6 by A27, 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:
A8: {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 A8, 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 A9: ( 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:
A10: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume ( z' <= x & z' <= y ) ; :: thesis:
then A11: ( z' c= 3 \ 1 & z' c= 2 ) by A9, YELLOW_1:3;

A12: now

assume z' = 3 \ 1 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A13: now

assume z' = 2 ; :: thesis:
then ( 0 in z' & not 0 in 3 \ 1 ) by CARD_1:88, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis:

end;

A00: now

assume z' = 1 ; :: thesis:
then ( 0 in z' & not 0 in 3 \ 1 ) by CARD_1:87, TARSKI:def 1, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis:

end;

now

assume z' = 3 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A11; :: thesis:

end;

hence z' <= z by A00, A10, A12, A13, A14, 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 AA, 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 Lem1, XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of B_6 by AA, 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 F1: ( x = 1 & y = 3 ) ; :: thesis:

1 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of B_6 by F1, 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 Lem1, XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of B_6 by AA, 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 F1: ( y = 1 & x = 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 A15: ( 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 A15;
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 A16: ( 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:
A17: z' is Element of {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume ( z' <= x & z' <= y ) ; :: thesis:
then A18: ( z' c= 3 \ 1 & z' c= 2 ) by A16, YELLOW_1:3;

A19: now

assume z' = 3 \ 1 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by TARSKI:def 2, YELLOW11:3;
hence contradiction by A18; :: thesis:

end;

A20: now

assume z' = 2 ; :: thesis:
then ( 0 in z' & not 0 in 3 \ 1 ) by CARD_1:88, TARSKI:def 2, YELLOW11:3;
hence contradiction by A18; :: thesis:

end;

A21: now

assume z' = 3 \ 2 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by TARSKI:def 1, YELLOW11:4;
hence contradiction by A18; :: thesis:

end;

A202: now

assume z' = 3 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by CARD_1:89, ENUMSET1:def 1;
hence contradiction by A18; :: thesis:

end;

now

assume z' = 1 ; :: thesis:
then ( 0 in z' & not 0 in 3 \ 1 ) by CARD_1:87, TARSKI:def 1, TARSKI:def 2, YELLOW11:3;
hence contradiction by A18; :: thesis:

end;

hence z' <= z by A17, A19, A20, A21, A202, ENUMSET1:def 4; :: thesis:

end;

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

end;

suppose A22: ( 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 A22, 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 A23: ( x = 2 & y = 3 ) ; :: thesis:

2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of B_6 by A23, 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 A24: ( 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 A24, 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 A25: ( 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 A25;
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 A26: ( 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 A26;
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 A27: ( x = 3 & y = 2 ) ; :: thesis:

2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of B_6 by A27, 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 A28: ( 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 A28;
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 A1; :: thesis: