let L be Lattice; :: thesis: for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
let p be Element of L; :: thesis: ( L is upper-bounded implies Top (latt <.p.)) = Top L )
given q being Element of L such that A1: for r being Element of L holds
( q "\/" r = q & r "\/" q = q ) ; :: according to LATTICES:def 14 :: thesis: Top (latt <.p.)) = Top L
A2: L is 1_Lattice by A1, LATTICES:def 14;
then A3: ( q = Top L & latt <.p.) is 1_Lattice ) by A1, Th66, RLSUB_2:85;
( Top L in <.p.) & the carrier of (latt <.p.)) = <.p.) ) by A2, Th12, Th63;
then reconsider q' = Top L as Element of (latt <.p.)) ;

now

let r' be Element of (latt <.p.)); :: thesis: r' "\/" q' = q'
reconsider r = r' as Element of <.p.) by Th63;
thus r' "\/" q' = q "\/" r by A3, Th64
.= q' by A1, A3 ; :: thesis: verum

end;

hence Top (latt <.p.)) = Top L by RLSUB_2:85; :: thesis: verum