reconsider x = 0 as Element of Benzene by Th9, ENUMSET1:def 4;
for a being Element of Benzene holds
( x "/\" a = x & a "/\" x = x ) by Th25;
hence Bottom Benzene = 0 by LATTICES:def 16; :: thesis: verum