let L be Lattice; :: thesis: for p being Element of L holds FinMeet {.p.} = p
let p be Element of L; :: thesis: FinMeet {.p.} = p
set M = the L_meet of L;
A1: ( the L_meet of L is commutative & the L_meet of L is associative ) by LATTICE2:31, LATTICE2:32;
thus FinMeet {.p.} = the L_meet of L $$ {.p.},(id L) by LATTICE2:def 4
.= (id L) . p by A1, SETWISEO:26
.= p by TMAP_1:91 ; :: thesis: verum