theorem Th28: :: LATTICE2:28

for L being Lattice
for A being non empty set
for x being Element of A
for B being Element of Fin A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f) by SETWISEO:22;