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
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
LATTICE3:def 11 ex b1 being Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
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
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
(
z <= x &
z <= y & ( for
z9 being
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
z9 <= x &
z9 <= y holds
z9 <= z ) )
verumproof
per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) )
by A2, ENUMSET1:def 3;
suppose
(
x = 0 &
y = 0 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A4:
w <= x
and A5:
w <= y
;
w <= zA6:
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;
verum end; suppose
(
x = 0 &
y = 3
\ 1 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A8:
w <= x
and A9:
w <= y
;
w <= zA10:
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;
verum end; suppose
(
x = 0 &
y = 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A12:
w <= x
and A13:
w <= y
;
w <= zA14:
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;
verum end; suppose
(
x = 0 &
y = 3
\ 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A16:
w <= x
and A17:
w <= y
;
w <= zA18:
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;
verum end; suppose
(
x = 0 &
y = 3 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A20:
w <= x
and A21:
w <= y
;
w <= zA22:
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;
verum end; suppose
(
x = 3
\ 1 &
y = 0 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A24:
w <= x
and A25:
w <= y
;
w <= zA26:
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;
verum end; suppose
(
x = 3
\ 1 &
y = 3
\ 1 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A28:
w <= x
and A29:
w <= y
;
w <= zA30:
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;
verum end; suppose A31:
(
x = 3
\ 1 &
y = 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
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
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )A32:
z c= y
;
z c= x
;
hence
(
z <= x &
z <= y )
by A32, YELLOW_1:3;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet z9 be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( z9 <= x & z9 <= y implies z9 <= z )assume that A33:
z9 <= x
and A34:
z9 <= y
;
z9 <= zA35:
z9 c= 3
\ 1
by A31, A33, YELLOW_1:3;
A37:
z9 c= 2
by A31, A34, YELLOW_1:3;
A40:
now not z9 = 3 \ 2end; A42:
now not z9 = 3 \ 1end;
z9 is
Element of
{0,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
hence
z9 <= z
by A42, A36, A40, A38, ENUMSET1:def 3;
verum end; suppose
(
x = 3
\ 1 &
y = 3
\ 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) by Th3, Th4, ZFMISC_1:13;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A45:
w <= x
and A46:
w <= y
;
w <= zA47:
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;
verum end; suppose A48:
(
x = 3
\ 1 &
y = 3 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )(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 A48;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A50:
w <= x
and A51:
w <= y
;
w <= zA52:
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;
verum end; suppose
(
x = 2 &
y = 0 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A54:
w <= x
and A55:
w <= y
;
w <= zA56:
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;
verum end; suppose A57:
(
x = 2 &
y = 3
\ 1 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
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
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )A58:
z c= y
;
z c= x
;
hence
(
z <= x &
z <= y )
by A58, YELLOW_1:3;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet z9 be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( z9 <= x & z9 <= y implies z9 <= z )assume that A59:
z9 <= x
and A60:
z9 <= y
;
z9 <= zA61:
z9 c= 3
\ 1
by A57, A60, YELLOW_1:3;
A63:
z9 c= 2
by A57, A59, YELLOW_1:3;
A66:
now not z9 = 3 \ 2end; A68:
now not z9 = 3 \ 1end;
z9 is
Element of
{0,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;
hence
z9 <= z
by A68, A62, A66, A64, ENUMSET1:def 3;
verum end; suppose
(
x = 2 &
y = 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A71:
w <= x
and A72:
w <= y
;
w <= zA73:
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;
verum end; suppose A74:
(
x = 2 &
y = 3
\ 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
2
misses 3
\ 2
by XBOOLE_1:79;
then
2
/\ (3 \ 2) = 0
;
then
x /\ y in {0,(3 \ 1),2,(3 \ 2),3}
by A74, 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
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A76:
w <= x
and A77:
w <= y
;
w <= zA78:
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;
verum end; suppose A79:
(
x = 2 &
y = 3 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
Segm 2
c= Segm 3
by NAT_1:39;
then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) by A79, XBOOLE_1:28;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A81:
w <= x
and A82:
w <= y
;
w <= zA83:
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;
verum end; suppose
(
x = 3
\ 2 &
y = 0 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A85:
w <= x
and A86:
w <= y
;
w <= zA87:
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;
verum end; suppose
(
x = 3
\ 2 &
y = 3
\ 1 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) by Th3, Th4, ZFMISC_1:13;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A89:
w <= x
and A90:
w <= y
;
w <= zA91:
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;
verum end; suppose A92:
(
x = 3
\ 2 &
y = 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
2
misses 3
\ 2
by XBOOLE_1:79;
then
2
/\ (3 \ 2) = 0
;
then
x /\ y in {0,(3 \ 1),2,(3 \ 2),3}
by A92, 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
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A94:
w <= x
and A95:
w <= y
;
w <= zA96:
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;
verum end; suppose
(
x = 3
\ 2 &
y = 3
\ 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A98:
w <= x
and A99:
w <= y
;
w <= zA100:
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;
verum end; suppose A101:
(
x = 3
\ 2 &
y = 3 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )(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 A101;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A103:
w <= x
and A104:
w <= y
;
w <= zA105:
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;
verum end; suppose
(
x = 3 &
y = 0 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A107:
w <= x
and A108:
w <= y
;
w <= zA109:
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;
verum end; suppose A110:
(
x = 3 &
y = 3
\ 1 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )(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 A110;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A112:
w <= x
and A113:
w <= y
;
w <= zA114:
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;
verum end; suppose A115:
(
x = 3 &
y = 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )
Segm 2
c= Segm 3
by NAT_1:39;
then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) by A115, XBOOLE_1:28;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A117:
w <= x
and A118:
w <= y
;
w <= zA119:
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;
verum end; suppose A120:
(
x = 3 &
y = 3
\ 2 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )(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 A120;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A122:
w <= x
and A123:
w <= y
;
w <= zA124:
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;
verum end; suppose
(
x = 3 &
y = 3 )
;
ex z being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )then reconsider z =
x /\ y as
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3}) ;
take
z
;
( z <= x & z <= y & ( for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= z ) )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;
for z9 being Element of (InclPoset {0,(3 \ 1),2,(3 \ 2),3}) st z9 <= x & z9 <= y holds
z9 <= zlet w be
Element of
(InclPoset {0,(3 \ 1),2,(3 \ 2),3});
( w <= x & w <= y implies w <= z )assume that A126:
w <= x
and A127:
w <= y
;
w <= zA128:
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;
verum end; end;
end;
end;
now for x, y being set st x in {0,(3 \ 1),2,(3 \ 2),3} & y in {0,(3 \ 1),2,(3 \ 2),3} holds
x \/ y in {0,(3 \ 1),2,(3 \ 2),3}let x,
y be
set ;
( x in {0,(3 \ 1),2,(3 \ 2),3} & y in {0,(3 \ 1),2,(3 \ 2),3} implies x \/ y in {0,(3 \ 1),2,(3 \ 2),3} )assume that A129:
x in {0,(3 \ 1),2,(3 \ 2),3}
and A130:
y in {0,(3 \ 1),2,(3 \ 2),3}
;
x \/ y in {0,(3 \ 1),2,(3 \ 2),3}A131:
(
x = 0 or
x = 3
\ 1 or
x = 2 or
x = 3
\ 2 or
x = 3 )
by A129, ENUMSET1:def 3;
Segm 2
c= Segm 3
by NAT_1:39;
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:50, ENUMSET1:5
.=
{1,1,0,2}
by ENUMSET1:67
.=
{1,0,2}
by ENUMSET1:31
.=
{0,1,2}
by ENUMSET1:58
;
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:9;
hence
x \/ y in {0,(3 \ 1),2,(3 \ 2),3}
by A131, A136, A134, A135, A133, A132, A137, Th3, CARD_1:51, ENUMSET1:def 3;
verum end;
hence
( N_5 is with_infima & N_5 is with_suprema )
by A1, YELLOW_1:11; verum