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