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 LemBA, ENUMSET1:def 4;
hence a c= 3 by NAT_1:40; :: thesis: verum