reconsider B = 3 as Element of Benzene by Th9, ENUMSET1:def 4;
take B ; :: according to LATTICES:def 14 :: 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 Th27;
hence for b₁ being Element of the carrier of Benzene holds
( B "\/" b₁ = B & b₁ "\/" B = B ) ; :: thesis: verum