let L be Lattice; :: thesis: for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]
let p be Element of L; :: thesis: ( L is upper-bounded implies <.p.) = [#p,(Top L)#] )
assume A1: L is upper-bounded ; :: thesis: <.p.) = [#p,(Top L)#]
let q be Element of L; :: according to FILTER_2:def 1 :: thesis: ( q in <.p.) iff q in [#p,(Top L)#] )
( p [= Top L & q [= Top L ) by A1, LATTICES:45;
then ( ( q in <.p.) implies p [= q ) & ( p [= q implies q in <.p.) ) & ( q in [#p,(Top L)#] implies p [= q ) & ( p [= q implies q in [#p,(Top L)#] ) ) by Th63, FILTER_0:18;
hence ( q in <.p.) iff q in [#p,(Top L)#] ) ; :: thesis: verum