let L be Lattice; :: thesis: for p being Element of L holds FinJoin {.p.} = p
let p be Element of L; :: thesis: FinJoin {.p.} = p
set J = the L_join of L;
thus FinJoin {.p.} = the L_join of L $$ {.p.},(id L) by LATTICE2:def 3
.= (id L) . p by SETWISEO:26
.= p by FUNCT_1:35 ; :: thesis: verum