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