A2: LattStr(# the carrier of Benzene ,the L_join of Benzene ,the L_meet of Benzene #) = LattStr(# the carrier of (latt B_6 ),the L_join of (latt B_6 ),the L_meet of (latt B_6 ) #) by BenDef;
LattPOSet (latt B_6 ) = RelStr(# the carrier of B_6 ,the InternalRel of B_6 #) by LATTICE3:def 15;
hence the carrier of Benzene = {0 ,1,(3 \ 1),2,(3 \ 2),3} by A2, YELLOW_1:1; :: thesis: verum