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

proof

let x, y be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: according to LATTICE3:def 10 :: thesis:
A2: {0 ,1,(2 \ 1),(3 \ 2),3} = the carrier of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
thus ex z being Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) st
( x <= z & y <= z & ( for z' being Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) st x <= z' & y <= z' 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) ;
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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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 = 1 ) ; :: thesis:

end;

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

end;

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

end;

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

end;

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

end;

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

end;

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

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in x ; :: thesis:
then X = 0 by A3, CARD_1:87, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 1 by A3, Th2, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A4: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A5: ( 1 c= z' & 2 \ 1 c= z' ) by A3, YELLOW_1:3;
A6: z' <> 0 by A5;

A8: now

assume A9: z' = 1 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
then 1 in z' by A5;
hence contradiction by A9; :: thesis:

end;

A10: now

assume A11: z' = 2 \ 1 ; :: thesis:
0 in 1 by CARD_1:87, TARSKI:def 1;
hence contradiction by A5, A11, Th2, TARSKI:def 1; :: thesis:

end;

now

assume A12: z' = 3 \ 2 ; :: thesis:
0 in 1 by CARD_1:87, TARSKI:def 1;
hence contradiction by A5, A12, Th4, TARSKI:def 1; :: thesis:

end;

hence z <= z' by A4, A6, A8, A10, ENUMSET1:def 3; :: thesis:

end;

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

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in x ; :: thesis:
then X = 0 by A13, CARD_1:87, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

thus y c= z by A13; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A14: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A15: ( 1 c= z' & 3 \ 2 c= z' ) by A13, YELLOW_1:3;
A16: z' <> 0 by A15;

A18: now

assume A19: z' = 1 ; :: thesis:
2 in 3 \ 2 by Th4, TARSKI:def 1;
hence contradiction by A15, A19, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A20: now

assume A21: z' = 2 \ 1 ; :: thesis:
0 in 1 by CARD_1:87, TARSKI:def 1;
hence contradiction by A15, A21, Th2, TARSKI:def 1; :: thesis:

end;

now

assume A22: z' = 3 \ 2 ; :: thesis:
0 in 1 by CARD_1:87, TARSKI:def 1;
hence contradiction by A15, A22, Th4, TARSKI:def 1; :: thesis:

end;

hence z <= z' by A14, A16, A18, A20, ENUMSET1:def 3; :: thesis:

end;

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

1 c= 3

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in 1 ; :: thesis:
then X = 0 by CARD_1:87, TARSKI:def 1;
hence X in 3 by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

then reconsider z = x \/ y as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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 \ 1 & y = 0 ) ; :: thesis:

end;

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

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in x ; :: thesis:
then X = 1 by A24, Th2, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 0 by A24, CARD_1:87, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A25: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A26: ( 1 c= z' & 2 \ 1 c= z' ) by A24, YELLOW_1:3;
A27: z' <> 0 by A26;

A29: now

assume A30: z' = 1 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
then 1 in z' by A26;
hence contradiction by A30; :: thesis:

end;

A31: now

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

end;

now

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

end;

hence z <= z' by A25, A27, A29, A31, ENUMSET1:def 3; :: thesis:

end;

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

end;

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

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in x ; :: thesis:
then X = 1 by A34, Th2, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
hence X in z by A34; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A35: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A36: ( 2 \ 1 c= z' & 3 \ 2 c= z' ) by A34, YELLOW_1:3;
A37: z' <> 0 by Th2, A36;

A39: now

assume A40: z' = 1 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
then 1 in z' by A36;
hence contradiction by A40; :: thesis:

end;

A41: now

assume A42: z' = 2 \ 1 ; :: thesis:
2 in 3 \ 2 by Th4, TARSKI:def 1;
hence contradiction by A36, A42, Th2, TARSKI:def 1; :: thesis:

end;

now

assume A43: z' = 3 \ 2 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
hence contradiction by A36, A43, Th4, TARSKI:def 1; :: thesis:

end;

hence z <= z' by A35, A37, A39, A41, ENUMSET1:def 3; :: thesis:

end;

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

2 \ 1 c= 3

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in 2 \ 1 ; :: thesis:
then X = 1 by Th2, TARSKI:def 1;
hence X in 3 by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

then reconsider z = x \/ y as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by A44, 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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 A45: ( x = 3 \ 2 & y = 1 ) ; :: thesis:

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z by A45; :: thesis:
thus y c= z :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 0 by A45, CARD_1:87, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A46: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A47: ( 1 c= z' & 3 \ 2 c= z' ) by A45, YELLOW_1:3;
A48: z' <> 0 by A47;

A50: now

assume A51: z' = 1 ; :: thesis:
2 in 3 \ 2 by Th4, TARSKI:def 1;
hence contradiction by A47, A51, CARD_1:87, TARSKI:def 1; :: thesis:

end;

A52: now

assume A53: z' = 2 \ 1 ; :: thesis:
0 in 1 by CARD_1:87, TARSKI:def 1;
hence contradiction by A47, A53, Th2, TARSKI:def 1; :: thesis:

end;

now

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

end;

hence z <= z' by A46, A48, A50, A52, ENUMSET1:def 3; :: thesis:

end;

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

3 in {0 ,1,(2 \ 1),(3 \ 2),3} by ENUMSET1:def 3;
then reconsider z = 3 as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z by A55; :: thesis:
let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 1 by A55, Th2, TARSKI:def 1;
hence X in z by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: thesis:
A56: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
assume ( x <= z' & y <= z' ) ; :: thesis:
then A57: ( 2 \ 1 c= z' & 3 \ 2 c= z' ) by A55, YELLOW_1:3;
A58: z' <> 0 by Th2, A57;

A60: now

assume A61: z' = 1 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
then 1 in z' by A57;
hence contradiction by A61; :: thesis:

end;

A62: now

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

end;

now

assume A64: z' = 3 \ 2 ; :: thesis:
1 in 2 \ 1 by Th2, TARSKI:def 1;
hence contradiction by A57, A64, Th4, TARSKI:def 1; :: thesis:

end;

hence z <= z' by A56, A58, A60, A62, ENUMSET1:def 3; :: thesis:

end;

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

end;

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

then reconsider z = x \/ y as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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 = 0 ) ; :: thesis:

end;

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

1 c= 3

proof

end;

then reconsider z = x \/ y as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by A65, 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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 A66: ( x = 3 & y = 2 \ 1 ) ; :: thesis:

2 \ 1 c= 3

proof

end;

then reconsider z = x \/ y as Element of (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}) by A66, 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 (InclPoset {0 ,1,(2 \ 1),(3 \ 2),3}); :: 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;

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

proof

now

let x, y be set ; :: thesis:
assume ( x in {0 ,1,(2 \ 1),(3 \ 2),3} & y in {0 ,1,(2 \ 1),(3 \ 2),3} ) ; :: thesis:
then A67: ( ( x = 0 or x = 1 or x = 2 \ 1 or x = 3 \ 2 or x = 3 ) & ( y = 0 or y = 1 or y = 2 \ 1 or y = 3 \ 2 or y = 3 ) ) by ENUMSET1:def 3;
1 misses 2 \ 1 by XBOOLE_1:79;
then A68: 1 /\ (2 \ 1) = 0 by XBOOLE_0:def 7;
A69: 1 /\ (3 \ 2) = 0

proof

now

let x be set ; :: thesis:
assume x in 1 /\ (3 \ 2) ; :: thesis:
then ( x in 1 & x in 3 \ 2 ) by XBOOLE_0:def 4;
then ( x = 0 & x = 2 & 0 <> 2 ) by Th4, CARD_1:87, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

hence 1 /\ (3 \ 2) = 0 by XBOOLE_0:def 1; :: thesis:

end;

1 c= 3 by NAT_1:40;
then A70: 1 /\ 3 = 1 by XBOOLE_1:28;
A71: (2 \ 1) /\ (3 \ 2) = 0

proof

now

let x be set ; :: thesis:
assume x in (2 \ 1) /\ (3 \ 2) ; :: thesis:
then ( x in 2 \ 1 & x in 3 \ 2 ) by XBOOLE_0:def 4;
then ( x = 1 & x = 2 & 1 <> 2 ) by Th2, Th4, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

hence (2 \ 1) /\ (3 \ 2) = 0 by XBOOLE_0:def 1; :: thesis:

end;

2 \ 1 c= 3

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in 2 \ 1 ; :: thesis:
then x = 1 by Th2, TARSKI:def 1;
hence x in 3 by CARD_1:89, ENUMSET1:def 1; :: thesis:

end;

then A72: (2 \ 1) /\ 3 = 2 \ 1 by XBOOLE_1:28;
(3 \ 2) /\ 3 = 3 \ 2 by XBOOLE_1:28;
hence x /\ y in {0 ,1,(2 \ 1),(3 \ 2),3} by A67, A68, A69, A70, A71, A72, ENUMSET1:def 3; :: thesis:

end;

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

end;

hence ( M_3 is with_infima & M_3 is with_suprema ) by A1; :: thesis: