reconsider B = 0 as Element of Benzene by Th9, ENUMSET1:def 4;
take B ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of Benzene holds
( B "/\" b₁ = B & b₁ "/\" B = B )
for a being Element of Benzene holds
( B "/\" a = B & a "/\" B = B ) by Th25;
hence for b₁ being Element of the carrier of Benzene holds
( B "/\" b₁ = B & b₁ "/\" B = B ) ; :: thesis: verum