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