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