let L be Lattice; :: thesis: for p being Element of st L is upper-bounded holds
Top (latt <.p.)) = Top L
let p be Element of ; :: thesis: ( L is upper-bounded implies Top (latt <.p.)) = Top L )
given q being Element of such that A1: for r being Element of 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 Th12;
then reconsider q' = Top L as Element of by Th63;
A2: q = Top L by A1, RLSUB_2:85;

now

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

end;

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