theorem Th9: :: LATTICE4:9

for L being Lattice
for p being Element of L holds FinJoin {.p.} = p