let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of Benzene or a in bool 3 )
A1: ( 0 c= 3 & Segm 1 c= Segm 3 ) by NAT_1:39;
assume A2: a in the carrier of Benzene ; :: thesis: a in bool 3
A3: ( Segm 2 c= Segm 3 & 3 c= 3 ) by NAT_1:39;
( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by A2, Th9, ENUMSET1:def 4;
hence a in bool 3 by A1, A3; :: thesis: verum