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 ; :: 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 st
( x <= z & y <= z & ( for z' being Element of 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 ;
take z ; :: thesis:
A3: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A3, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A4: x <= w and
A5: y <= w ; :: thesis:
A6: y c= w by A5, YELLOW_1:3;
x c= w by A4, YELLOW_1:3;
then x \/ y c= w by A6, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

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

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A11: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A11, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A12: x <= w and
A13: y <= w ; :: thesis:
A14: y c= w by A13, YELLOW_1:3;
x c= w by A12, YELLOW_1:3;
then x \/ y c= w by A14, XBOOLE_1:8;
hence z <= w 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: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A15, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A16: x <= w and
A17: y <= w ; :: thesis:
A18: y c= w by A17, YELLOW_1:3;
x c= w by A16, YELLOW_1:3;
then x \/ y c= w by A18, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

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

end;

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

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

end;

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

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

end;

suppose A31: ( 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 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 A31, 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 A31, 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 ; :: thesis:
assume that
A32: x <= z' and
A33: y <= z' ; :: thesis:
A34: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A35: 2 \ 1 c= z' by A31, A33, YELLOW_1:3;

A36: now

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

end;

A38: 1 c= z' by A31, A32, YELLOW_1:3;

A39: now

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

end;

A41: now

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

end;

z' <> 0 by A38;
hence z <= z' by A34, A36, A39, A41, ENUMSET1:def 3; :: thesis:

end;

suppose A43: ( 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 by YELLOW_1:1;
take z ; :: thesis:
x c= z

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in x ; :: thesis:
then X = 0 by A43, 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 A43, YELLOW_1:3; :: thesis:
let z' be Element of ; :: thesis:
assume that
A44: x <= z' and
A45: y <= z' ; :: thesis:
A46: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A47: 3 \ 2 c= z' by A43, A45, YELLOW_1:3;

A48: now

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

end;

A50: 1 c= z' by A43, A44, YELLOW_1:3;

A51: now

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

end;

A53: now

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

end;

z' <> 0 by A50;
hence z <= z' by A46, A48, A51, A53, ENUMSET1:def 3; :: thesis:

end;

suppose A55: ( 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 by A55, XBOOLE_1:12;
take z ; :: thesis:
A56: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A56, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A57: x <= w and
A58: y <= w ; :: thesis:
A59: y c= w by A58, YELLOW_1:3;
x c= w by A57, YELLOW_1:3;
then x \/ y c= w by A59, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A60: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A60, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A61: x <= w and
A62: y <= w ; :: thesis:
A63: y c= w by A62, YELLOW_1:3;
x c= w by A61, YELLOW_1:3;
then x \/ y c= w by A63, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A64: ( 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 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 A64, 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 A64, 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 ; :: thesis:
assume that
A65: x <= z' and
A66: y <= z' ; :: thesis:
A67: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A68: 2 \ 1 c= z' by A64, A65, YELLOW_1:3;

A69: now

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

end;

A71: 1 c= z' by A64, A66, YELLOW_1:3;

A72: now

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

end;

A74: now

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

end;

z' <> 0 by A71;
hence z <= z' by A67, A69, A72, A74, ENUMSET1:def 3; :: thesis:

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A76: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A76, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A77: x <= w and
A78: y <= w ; :: thesis:
A79: y c= w by A78, YELLOW_1:3;
x c= w by A77, YELLOW_1:3;
then x \/ y c= w by A79, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A80: ( 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 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 A80, 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 A80; :: thesis:

end;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis:
let z' be Element of ; :: thesis:
assume that
A81: x <= z' and
A82: y <= z' ; :: thesis:
A83: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A84: 3 \ 2 c= z' by A80, A82, YELLOW_1:3;

A85: now

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

end;

A87: 2 \ 1 c= z' by A80, A81, YELLOW_1:3;

A88: now

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

end;

A90: now

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

end;

z' <> 0 by A87, Th2;
hence z <= z' by A83, A90, A85, A88, ENUMSET1:def 3; :: thesis:

end;

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

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A97: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A97, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A98: x <= w and
A99: y <= w ; :: thesis:
A100: y c= w by A99, YELLOW_1:3;
x c= w by A98, YELLOW_1:3;
then x \/ y c= w by A100, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A101: ( 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 by YELLOW_1:1;
take z ; :: thesis:
y c= z

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 0 by A101, 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 A101, YELLOW_1:3; :: thesis:
let z' be Element of ; :: thesis:
assume that
A102: x <= z' and
A103: y <= z' ; :: thesis:
A104: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A105: 3 \ 2 c= z' by A101, A102, YELLOW_1:3;

A106: now

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

end;

A108: 1 c= z' by A101, A103, YELLOW_1:3;

A109: now

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

end;

A111: now

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

end;

z' <> 0 by A108;
hence z <= z' by A104, A106, A109, A111, ENUMSET1:def 3; :: thesis:

end;

suppose A113: ( 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 by YELLOW_1:1;
take z ; :: thesis:
( x c= z & y c= z )

proof

thus x c= z by A113; :: thesis:
let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in y ; :: thesis:
then X = 1 by A113, 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 ; :: thesis:
assume that
A114: x <= z' and
A115: y <= z' ; :: thesis:
A116: z' is Element of {0 ,1,(2 \ 1),(3 \ 2),3} by YELLOW_1:1;
A117: 3 \ 2 c= z' by A113, A114, YELLOW_1:3;

A118: now

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

end;

A120: 2 \ 1 c= z' by A113, A115, YELLOW_1:3;

A121: now

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

end;

A123: now

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

end;

z' <> 0 by A120, Th2;
hence z <= z' by A116, A123, A118, A121, ENUMSET1:def 3; :: thesis:

end;

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

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

end;

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

then reconsider z = x \/ y as Element of by XBOOLE_1:12;
take z ; :: thesis:
A129: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A129, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A130: x <= w and
A131: y <= w ; :: thesis:
A132: y c= w by A131, YELLOW_1:3;
x c= w by A130, YELLOW_1:3;
then x \/ y c= w by A132, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A133: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A133, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A134: x <= w and
A135: y <= w ; :: thesis:
A136: y c= w by A135, YELLOW_1:3;
x c= w by A134, YELLOW_1:3;
then x \/ y c= w by A136, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A137: ( x = 3 & y = 1 ) ; :: 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 by A137, XBOOLE_1:12;
take z ; :: thesis:
A138: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A138, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A139: x <= w and
A140: y <= w ; :: thesis:
A141: y c= w by A140, YELLOW_1:3;
x c= w by A139, YELLOW_1:3;
then x \/ y c= w by A141, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

suppose A142: ( x = 3 & y = 2 \ 1 ) ; :: 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 by A142, XBOOLE_1:12;
take z ; :: thesis:
A143: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A143, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A144: x <= w and
A145: y <= w ; :: thesis:
A146: y c= w by A145, YELLOW_1:3;
x c= w by A144, YELLOW_1:3;
then x \/ y c= w by A146, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x \/ y as Element of by XBOOLE_1:12;
take z ; :: thesis:
A147: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A147, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A148: x <= w and
A149: y <= w ; :: thesis:
A150: y c= w by A149, YELLOW_1:3;
x c= w by A148, YELLOW_1:3;
then x \/ y c= w by A150, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

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

then reconsider z = x \/ y as Element of ;
take z ; :: thesis:
A151: y c= z by XBOOLE_1:7;
x c= z by XBOOLE_1:7;
hence ( x <= z & y <= z ) by A151, YELLOW_1:3; :: thesis:
let w be Element of ; :: thesis:
assume that
A152: x <= w and
A153: y <= w ; :: thesis:
A154: y c= w by A153, YELLOW_1:3;
x c= w by A152, YELLOW_1:3;
then x \/ y c= w by A154, XBOOLE_1:8;
hence z <= w by YELLOW_1:3; :: thesis:

end;

now

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

end;

then A157: (2 \ 1) /\ (3 \ 2) = 0 by XBOOLE_0:def 1;
A158: (3 \ 2) /\ 3 = 3 \ 2 by XBOOLE_1:28;
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 A159: (2 \ 1) /\ 3 = 2 \ 1 by XBOOLE_1:28;
1 c= 3 by NAT_1:40;
then A160: 1 /\ 3 = 1 by XBOOLE_1:28;

now

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

end;

then A163: 1 /\ (3 \ 2) = 0 by XBOOLE_0:def 1;
1 misses 2 \ 1 by XBOOLE_1:79;
then A164: 1 /\ (2 \ 1) = 0 by XBOOLE_0:def 7;
let x, y be set ; :: thesis:
assume that
A165: x in {0 ,1,(2 \ 1),(3 \ 2),3} and
A166: y in {0 ,1,(2 \ 1),(3 \ 2),3} ; :: thesis:
A167: ( y = 0 or y = 1 or y = 2 \ 1 or y = 3 \ 2 or y = 3 ) by A166, ENUMSET1:def 3;
( x = 0 or x = 1 or x = 2 \ 1 or x = 3 \ 2 or x = 3 ) by A165, ENUMSET1:def 3;
hence x /\ y in {0 ,1,(2 \ 1),(3 \ 2),3} by A167, A164, A163, A160, A157, A159, A158, ENUMSET1:def 3; :: thesis:

end;

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