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_infima

proof

let x, y be Element of ; :: according to LATTICE3:def 11 :: thesis:
A2: {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 st
( z <= x & z <= y & ( for z' being Element of st z' <= x & z' <= y holds
z' <= z ) ) :: thesis:

proof

per cases by A2, ENUMSET1:def 3;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A3: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A3, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A4: w <= x and
A5: w <= y ; :: thesis:
A6: w c= y by A5, YELLOW_1:3;
w c= x by A4, YELLOW_1:3;
then w c= x /\ y by A6, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A7: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A7, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A8: w <= x and
A9: w <= y ; :: thesis:
A10: w c= y by A9, YELLOW_1:3;
w c= x by A8, YELLOW_1:3;
then w c= x /\ y by A10, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A11: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A11, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A12: w <= x and
A13: w <= y ; :: thesis:
A14: w c= y by A13, YELLOW_1:3;
w c= x by A12, YELLOW_1:3;
then w c= x /\ y by A14, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A15: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A15, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A16: w <= x and
A17: w <= y ; :: thesis:
A18: w c= y by A17, YELLOW_1:3;
w c= x by A16, YELLOW_1:3;
then w c= x /\ y by A18, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A19: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A19, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A20: w <= x and
A21: w <= y ; :: thesis:
A22: w c= y by A21, YELLOW_1:3;
w c= x by A20, YELLOW_1:3;
then w c= x /\ y by A22, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A23: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A23, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A24: w <= x and
A25: w <= y ; :: thesis:
A26: w c= y by A25, YELLOW_1:3;
w c= x by A24, YELLOW_1:3;
then w c= x /\ y by A26, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A27: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A27, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A28: w <= x and
A29: w <= y ; :: thesis:
A30: w c= y by A29, YELLOW_1:3;
w c= x by A28, YELLOW_1:3;
then w c= x /\ y by A30, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A31: ( 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 by YELLOW_1:1;
take z ; :: thesis:
A32: z c= y by XBOOLE_1:2;
z c= x by XBOOLE_1:2;
hence ( z <= x & z <= y ) by A32, YELLOW_1:3; :: thesis:
let z' be Element of ; :: thesis:
assume that
A33: z' <= x and
A34: z' <= y ; :: thesis:
A35: z' c= 3 \ 1 by A31, A33, YELLOW_1:3;

A36: now

assume z' = 2 ; :: thesis:
then 0 in z' by CARD_1:88, TARSKI:def 2;
hence contradiction by A35, Th3, TARSKI:def 2; :: thesis:

end;

A37: z' c= 2 by A31, A34, YELLOW_1:3;

A38: now

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

end;

A40: now

assume z' = 3 \ 2 ; :: thesis:
then A41: 2 in z' by Th4, TARSKI:def 1;
not 2 in 2 ;
hence contradiction by A37, A41; :: thesis:

end;

A42: now

assume z' = 3 \ 1 ; :: thesis:
then A43: 2 in z' by Th3, TARSKI:def 2;
not 2 in 2 ;
hence contradiction by A37, A43; :: thesis:

end;

z' is Element of {0 ,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence z' <= z by A42, A36, A40, A38, ENUMSET1:def 3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of by Th3, Th4, ZFMISC_1:19;
take z ; :: thesis:
A44: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A44, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A45: w <= x and
A46: w <= y ; :: thesis:
A47: w c= y by A46, YELLOW_1:3;
w c= x by A45, YELLOW_1:3;
then w c= x /\ y by A47, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A48: ( 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 by A48;
take z ; :: thesis:
A49: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A49, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A50: w <= x and
A51: w <= y ; :: thesis:
A52: w c= y by A51, YELLOW_1:3;
w c= x by A50, YELLOW_1:3;
then w c= x /\ y by A52, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A53: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A53, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A54: w <= x and
A55: w <= y ; :: thesis:
A56: w c= y by A55, YELLOW_1:3;
w c= x by A54, YELLOW_1:3;
then w c= x /\ y by A56, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A57: ( 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 by YELLOW_1:1;
take z ; :: thesis:
A58: z c= y by XBOOLE_1:2;
z c= x by XBOOLE_1:2;
hence ( z <= x & z <= y ) by A58, YELLOW_1:3; :: thesis:
let z' be Element of ; :: thesis:
assume that
A59: z' <= x and
A60: z' <= y ; :: thesis:
A61: z' c= 3 \ 1 by A57, A60, YELLOW_1:3;

A62: now

assume z' = 2 ; :: thesis:
then 0 in z' by CARD_1:88, TARSKI:def 2;
hence contradiction by A61, Th3, TARSKI:def 2; :: thesis:

end;

A63: z' c= 2 by A57, A59, YELLOW_1:3;

A64: now

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

end;

A66: now

assume z' = 3 \ 2 ; :: thesis:
then A67: 2 in z' by Th4, TARSKI:def 1;
not 2 in 2 ;
hence contradiction by A63, A67; :: thesis:

end;

A68: now

assume z' = 3 \ 1 ; :: thesis:
then A69: 2 in z' by Th3, TARSKI:def 2;
not 2 in 2 ;
hence contradiction by A63, A69; :: thesis:

end;

z' is Element of {0 ,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence z' <= z by A68, A62, A66, A64, ENUMSET1:def 3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A70: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A70, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A71: w <= x and
A72: w <= y ; :: thesis:
A73: w c= y by A72, YELLOW_1:3;
w c= x by A71, YELLOW_1:3;
then w c= x /\ y by A73, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A74: ( 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 A74, ENUMSET1:def 3;
then reconsider z = x /\ y as Element of by YELLOW_1:1;
take z ; :: thesis:
A75: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A75, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A76: w <= x and
A77: w <= y ; :: thesis:
A78: w c= y by A77, YELLOW_1:3;
w c= x by A76, YELLOW_1:3;
then w c= x /\ y by A78, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of by A79, XBOOLE_1:28;
take z ; :: thesis:
A80: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A80, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A81: w <= x and
A82: w <= y ; :: thesis:
A83: w c= y by A82, YELLOW_1:3;
w c= x by A81, YELLOW_1:3;
then w c= x /\ y by A83, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A84: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A84, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A85: w <= x and
A86: w <= y ; :: thesis:
A87: w c= y by A86, YELLOW_1:3;
w c= x by A85, YELLOW_1:3;
then w c= x /\ y by A87, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of by Th3, Th4, ZFMISC_1:19;
take z ; :: thesis:
A88: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A88, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A89: w <= x and
A90: w <= y ; :: thesis:
A91: w c= y by A90, YELLOW_1:3;
w c= x by A89, YELLOW_1:3;
then w c= x /\ y by A91, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A92: ( 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 A92, ENUMSET1:def 3;
then reconsider z = x /\ y as Element of by YELLOW_1:1;
take z ; :: thesis:
A93: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A93, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A94: w <= x and
A95: w <= y ; :: thesis:
A96: w c= y by A95, YELLOW_1:3;
w c= x by A94, YELLOW_1:3;
then w c= x /\ y by A96, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A97: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A97, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A98: w <= x and
A99: w <= y ; :: thesis:
A100: w c= y by A99, YELLOW_1:3;
w c= x by A98, YELLOW_1:3;
then w c= x /\ y by A100, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: 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 by A101;
take z ; :: thesis:
A102: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A102, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A103: w <= x and
A104: w <= y ; :: thesis:
A105: w c= y by A104, YELLOW_1:3;
w c= x by A103, YELLOW_1:3;
then w c= x /\ y by A105, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A106: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A106, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A107: w <= x and
A108: w <= y ; :: thesis:
A109: w c= y by A108, YELLOW_1:3;
w c= x by A107, YELLOW_1:3;
then w c= x /\ y by A109, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A110: ( 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 by A110;
take z ; :: thesis:
A111: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A111, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A112: w <= x and
A113: w <= y ; :: thesis:
A114: w c= y by A113, YELLOW_1:3;
w c= x by A112, YELLOW_1:3;
then w c= x /\ y by A114, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of by A115, XBOOLE_1:28;
take z ; :: thesis:
A116: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A116, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A117: w <= x and
A118: w <= y ; :: thesis:
A119: w c= y by A118, YELLOW_1:3;
w c= x by A117, YELLOW_1:3;
then w c= x /\ y by A119, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

suppose A120: ( 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 by A120;
take z ; :: thesis:
A121: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A121, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A122: w <= x and
A123: w <= y ; :: thesis:
A124: w c= y by A123, YELLOW_1:3;
w c= x by A122, YELLOW_1:3;
then w c= x /\ y by A124, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x /\ y as Element of ;
take z ; :: thesis:
A125: z c= y by XBOOLE_1:17;
z c= x by XBOOLE_1:17;
hence ( z <= x & z <= y ) by A125, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A126: w <= x and
A127: w <= y ; :: thesis:
A128: w c= y by A127, YELLOW_1:3;
w c= x by A126, YELLOW_1:3;
then w c= x /\ y by A128, XBOOLE_1:19;
hence w <= z by YELLOW_1:3; :: thesis:

end;

now

let x, y be set ; :: thesis:
assume that
A129: x in {0 ,(3 \ 1),2,(3 \ 2),3} and
A130: y in {0 ,(3 \ 1),2,(3 \ 2),3} ; :: thesis:
A131: ( x = 0 or x = 3 \ 1 or x = 2 or x = 3 \ 2 or x = 3 ) by A129, ENUMSET1:def 3;
2 c= 3 by NAT_1:40;
then A132: 2 \/ 3 = 3 by XBOOLE_1:12;
A133: 2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39;
A134: (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 ;
A135: (3 \ 1) \/ 3 = 3 by XBOOLE_1:12;
A136: ( y = 0 or y = 3 \ 1 or y = 2 or y = 3 \ 2 or y = 3 ) by A130, ENUMSET1:def 3;
A137: (3 \ 2) \/ 3 = 3 by XBOOLE_1:12;
(3 \ 1) \/ (3 \ 2) = {1,2} by Th3, Th4, ZFMISC_1:14;
hence x \/ y in {0 ,(3 \ 1),2,(3 \ 2),3} by A131, A136, A134, A135, A133, A132, A137, Th3, CARD_1:89, ENUMSET1:def 3; :: thesis:

end;

hence ( N_5 is with_infima & N_5 is with_suprema ) by A1, YELLOW_1:11; :: thesis: