let L be Lattice; :: thesis: for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]
let p be Element of L; :: thesis: ( L is lower-bounded implies (.p.> = [#(Bottom L),p#] )
assume A1: L is lower-bounded ; :: thesis: (.p.> = [#(Bottom L),p#]
let q be Element of L; :: according to FILTER_2:def 1 :: thesis: ( q in (.p.> iff q in [#(Bottom L),p#] )
( Bottom L [= p & Bottom L [= q ) by A1, LATTICES:41;
then ( ( q in (.p.> implies q [= p ) & ( q [= p implies q in (.p.> ) & ( q in [#(Bottom L),p#] implies q [= p ) & ( q [= p implies q in [#(Bottom L),p#] ) ) by Th29, Th63;
hence ( q in (.p.> iff q in [#(Bottom L),p#] ) ; :: thesis: verum