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