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 Th63;
then reconsider p9 = p as Element of (latt <.p.)) by Th19;
reconsider q = q9 as Element of <.p.) by Th63;
q9 "/\" p9 = q9 by A1;
then q9 [= p9 by LATTICES:4;
then A2: q [= p by Th65;
A3: p [= q by Th18;
q9 = Bottom (latt <.p.)) by A1, RLSUB_2:64;
hence Bottom (latt <.p.)) = p by A2, A3, LATTICES:8; :: thesis: verum