:: deftheorem defines .: LATTICE2:def 2 :
for L being LattStr holds L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #);