let
a
be
set
;
:: thesis:
(
a
in
the
carrier
of
(
latt
B_6
)
implies
a
c=
Segm
3 )
assume
a
in
the
carrier
of
(
latt
B_6
)
;
:: thesis:
a
c=
Segm
3
then
(
a
=
0
or
a
=
Segm
1 or
a
=
3
\
1 or
a
=
Segm
2 or
a
=
3
\
2 or
a
=
3 )
by
Th7
,
ENUMSET1:def 4
;
hence
a
c=
Segm
3
by
NAT_1:39
;
:: thesis:
verum