reconsider B = 0 as Element of Benzene by Th9, ENUMSET1:def 4;

take B ; :: according to LATTICES:def 13 :: thesis: for b_{1} being Element of the carrier of Benzene holds

( B "/\" b_{1} = B & b_{1} "/\" B = B )

for a being Element of Benzene holds

( B "/\" a = B & a "/\" B = B ) by Th25;

hence for b_{1} being Element of the carrier of Benzene holds

( B "/\" b_{1} = B & b_{1} "/\" B = B )
; :: thesis: verum

take B ; :: according to LATTICES:def 13 :: thesis: for b

( B "/\" b

for a being Element of Benzene holds

( B "/\" a = B & a "/\" B = B ) by Th25;

hence for b

( B "/\" b