reconsider x = 3 as Element of Benzene by LemBen, ENUMSET1:def 4;
for a being Element of Benzene holds
( x "\/" a = x & a "\/" x = x ) by Bot1;
hence Top Benzene = 3 by LATTICES:def 17; :: thesis: verum