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;

thus FinMeet {.p.} = the L_meet of L $$ ({.p.},(id L)) by LATTICE2:def 4

.= (id L) . p by SETWISEO:17

.= p by FUNCT_1:18 ; :: thesis: verum

let p be Element of L; :: thesis: FinMeet {.p.} = p

set M = the L_meet of L;

thus FinMeet {.p.} = the L_meet of L $$ ({.p.},(id L)) by LATTICE2:def 4

.= (id L) . p by SETWISEO:17

.= p by FUNCT_1:18 ; :: thesis: verum