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