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
L is 1_Lattice by A1, LATTICES:def 14;
then Top L in <.p.) by Th11;
then reconsider q9 = Top L as Element of (latt <.p.)) by Th49;
A2: q = Top L by A1, RLSUB_2:65;

now :: thesis: for r9 being Element of (latt <.p.)) holds r9 "\/" q9 = q9

let r9 be Element of (latt <.p.)); :: thesis: r9 "\/" q9 = q9
reconsider r = r9 as Element of <.p.) by Th49;
thus r9 "\/" q9 = q "\/" r by A2, Th50
.= q9 by A1, A2 ; :: thesis: verum

end;

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