( 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) #) & LattPOSet (latt B_6) = RelStr(# the carrier of B_6, the InternalRel of B_6 #) ) by Def4, LATTICE3:def 15;
hence the carrier of Benzene = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1; :: thesis: verum