let L be Lattice; :: thesis: for p being Element of L holds Bottom (latt <.p.)) = p
let p be Element of L; :: thesis: Bottom (latt <.p.)) = p
consider q9 being Element of (latt <.p.)) such that
A1: for r9 being Element of (latt <.p.)) holds
( q9 "/\" r9 = q9 & r9 "/\" q9 = q9 ) by LATTICES:def 13;
the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider p9 = p as Element of (latt <.p.)) by Th16;
reconsider q = q9 as Element of <.p.) by Th49;
q9 "/\" p9 = q9 by A1;
then q9 [= p9 by LATTICES:4;
then A2: q [= p by Th51;
A3: p [= q by Th15;
q9 = Bottom (latt <.p.)) by A1, RLSUB_2:64;
hence Bottom (latt <.p.)) = p by A2, A3, LATTICES:8; :: thesis: verum