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
latt <.p.) is 0_Lattice by Th70;
then consider q' being Element of (latt <.p.)) such that
A1: for r' being Element of (latt <.p.)) holds
( q' "/\" r' = q' & r' "/\" q' = q' ) by LATTICES:def 13;
A2: the carrier of (latt <.p.)) = <.p.) by Th63;
A3: q' = Bottom (latt <.p.)) by A1, RLSUB_2:84;
reconsider p' = p as Element of (latt <.p.)) by A2, Th19;
reconsider q = q' as Element of <.p.) by Th63;
q' "/\" p' = q' by A1;
then q' [= p' by LATTICES:21;
then ( q [= p & p [= q ) by Th18, Th65;
hence Bottom (latt <.p.)) = p by A3, LATTICES:26; :: thesis: verum