let L be Lattice; :: thesis: for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )
let p be Element of L; :: thesis: ( L is lower-bounded implies ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) )
assume A1: L is lower-bounded ; :: thesis: ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )
then A2: L .: is upper-bounded by LATTICE2:63;
then A3: latt <.(p .:).) is upper-bounded by FILTER_0:66;
A4: latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th71
.= (latt ((L .:),<.(p .:).))) .: by Th30
.= (latt <.(p .:).)) .: by Th70 ;
hence latt (L,(.p.>) is lower-bounded by A3, LATTICE2:64; :: thesis: Bottom (latt (L,(.p.>)) = Bottom L
Top (latt <.(p .:).)) = Top (L .:) by A2, FILTER_0:72;
hence Bottom (latt (L,(.p.>)) = Top (L .:) by A4, A3, LATTICE2:79
.= Bottom L by A1, LATTICE2:78 ;
:: thesis: verum