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 ) )
A1: latt L,(.p.> = (latt (L .: ),((.p.> .: )) .: by Th71
.= (latt (L .: ),<.(p .: ).)) .: by Th30
.= (latt <.(p .: ).)) .: by Th70 ;
assume A2: L is lower-bounded ; :: thesis: ( latt L,(.p.> is lower-bounded & Bottom (latt L,(.p.>) = Bottom L )
then A3: L .: is upper-bounded by LATTICE2:63;
then A4: latt <.(p .: ).) is upper-bounded by FILTER_0:66;
hence latt L,(.p.> is lower-bounded by A1, LATTICE2:64; :: thesis: Bottom (latt L,(.p.>) = Bottom L
Top (latt <.(p .: ).)) = Top (L .: ) by A3, FILTER_0:72;
hence Bottom (latt L,(.p.>) = Top (L .: ) by A1, A4, LATTICE2:79
.= Bottom L by A2, LATTICE2:78 ;
:: thesis: verum