:: deftheorem defines FinJoin LATTICE4:def 8 :
for L being Lattice
for B being Element of Fin the carrier of L holds FinJoin B = FinJoin (B,(id L));