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