set Z = {0 ,(3 \ 1),2,(3 \ 2),3};
set N = InclPoset {0 ,(3 \ 1),2,(3 \ 2),3};
A1: InclPoset {0 ,(3 \ 1),2,(3 \ 2),3} is with_suprema

proof

now

let x, y be set ; :: thesis:
assume ( x in {0 ,(3 \ 1),2,(3 \ 2),3} & y in {0 ,(3 \ 1),2,(3 \ 2),3} ) ; :: thesis:
then A2: ( ( x = 0 or x = 3 \ 1 or x = 2 or x = 3 \ 2 or x = 3 ) & ( y = 0 or y = 3 \ 1 or y = 2 or y = 3 \ 2 or y = 3 ) ) by ENUMSET1:def 3;
A3: (3 \ 1) \/ 2 = {0 ,1,1,2} by Th3, CARD_1:88, ENUMSET1:45
.= {1,1,0 ,2} by ENUMSET1:110
.= {1,0 ,2} by ENUMSET1:71
.= {0 ,1,2} by ENUMSET1:99 ;
A4: (3 \ 1) \/ (3 \ 2) = {1,2} by Th3, Th4, ZFMISC_1:14;
A5: (3 \ 1) \/ 3 = 3 by XBOOLE_1:12;
A6: ( 2 \/ (3 \ 2) = 2 \/ 3 & 2 c= 3 ) by NAT_1:40, XBOOLE_1:39;
then A7: 2 \/ 3 = 3 by XBOOLE_1:12;
(3 \ 2) \/ 3 = 3 by XBOOLE_1:12;
hence x \/ y in {0 ,(3 \ 1),2,(3 \ 2),3} by A2, A3, A4, A5, A6, A7, Th3, CARD_1:89, ENUMSET1:def 3; :: thesis:

end;

hence InclPoset {0 ,(3 \ 1),2,(3 \ 2),3} is with_suprema by YELLOW_1:11; :: thesis:

end;

InclPoset {0 ,(3 \ 1),2,(3 \ 2),3} is with_infima

proof

let x, y be Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: according to LATTICE3:def 11 :: thesis:
A8: {0 ,(3 \ 1),2,(3 \ 2),3} = the carrier of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) by YELLOW_1:1;
thus ex z being Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z' being Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) st z' <= x & z' <= y holds
z' <= z ) ) :: thesis:

proof

per cases by A8, ENUMSET1:def 3;

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

then reconsider z = x /\ y as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) ;
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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 ,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 0 as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: thesis:
A10: z' is Element of {0 ,(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 Th3, TARSKI:def 2;
hence contradiction by A11; :: thesis:

end;

A13: now

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

end;

A14: now

assume z' = 3 \ 2 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by Th4, TARSKI:def 1;
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 A10, A12, A13, A14, ENUMSET1:def 3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) by Th3, Th4, 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 ,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 0 as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: thesis:
A17: z' is Element of {0 ,(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 Th3, TARSKI:def 2;
hence contradiction by A18; :: thesis:

end;

A20: now

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

end;

A21: now

assume z' = 3 \ 2 ; :: thesis:
then ( 2 in z' & not 2 in 2 ) by Th4, TARSKI:def 1;
hence contradiction by A18; :: 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 A18; :: thesis:

end;

hence z' <= z by A17, A19, A20, A21, ENUMSET1:def 3; :: 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 ,(3 \ 1),2,(3 \ 2),3} by A22, ENUMSET1:def 3;
then reconsider z = x /\ y as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 ,(3 \ 1),2,(3 \ 2),3} by A24, ENUMSET1:def 3;
then reconsider z = x /\ y as Element of (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}) 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 (InclPoset {0 ,(3 \ 1),2,(3 \ 2),3}); :: 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 ( N_5 is with_infima & N_5 is with_suprema ) by A1; :: thesis: