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