LattPOSet LattStr(# the carrier of Benzene ,the L_join of Benzene ,the L_meet of Benzene #) = LattPOSet (latt B_6 ) by Def4;
hence LattPOSet LattStr(# the carrier of Benzene ,the L_join of Benzene ,the L_meet of Benzene #) = B_6 by LATTICE3:def 15; :: thesis: verum