let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of Benzene or a in bool 3 )
assume A1: a in the carrier of Benzene ; :: thesis: a in bool 3
then reconsider x = a as Element of Benzene ;
A2: ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by LemBen, A1, ENUMSET1:def 4;
( 0 c= 3 & 1 c= 3 & 2 c= 3 & 3 c= 3 ) by NAT_1:40;
hence a in bool 3 by A2; :: thesis: verum