theorem :: LATTICE2:36

for A being non empty set
for L being Lattice
for B being Element of Fin A
for f being Function of A, the carrier of L
for f9 being Function of A, the carrier of (L .:) st f = f9 holds
( FinJoin (B,f) = FinMeet (B,f9) & FinMeet (B,f) = FinJoin (B,f9) ) ;