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:48;
then A3: latt <.(p .:).) is upper-bounded by FILTER_0:52;
A4: latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70
.= (latt ((L .:),<.(p .:).))) .: by Th29
.= (latt <.(p .:).)) .: by Th69 ;
hence latt (L,(.p.>) is lower-bounded by A3, LATTICE2:49; :: thesis: Bottom (latt (L,(.p.>)) = Bottom L
Top (latt <.(p .:).)) = Top (L .:) by A2, FILTER_0:57;
hence Bottom (latt (L,(.p.>)) = Top (L .:) by A4, A3, LATTICE2:62
.= Bottom L by A1, LATTICE2:61 ;
:: thesis: verum