let L be Lattice; for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]
let p be Element of L; ( L is upper-bounded implies <.p.) = [#p,(Top L)#] )
assume A1:
L is upper-bounded
; <.p.) = [#p,(Top L)#]
let q be Element of L; FILTER_2:def 1 ( q in <.p.) iff q in [#p,(Top L)#] )
A2:
( q in <.p.) iff p [= q )
by FILTER_0:15;
( p [= Top L & q [= Top L )
by A1, LATTICES:19;
hence
( q in <.p.) iff q in [#p,(Top L)#] )
by A2, Th62; verum