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#] )
A2: ( q in (.p.> iff q [= p ) by Th28;
( Bottom L [= p & Bottom L [= q ) by A1;
hence ( q in (.p.> iff q in [#(Bottom L),p#] ) by A2, Th62; :: thesis: verum