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

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