let L be Lattice; :: thesis: for I being non empty ClosedSubset of L st L is upper-bounded & Top L in I holds
( latt (L,I) is upper-bounded & Top (latt (L,I)) = Top L )
let I be non empty ClosedSubset of L; :: thesis: ( L is upper-bounded & Top L in I implies ( latt (L,I) is upper-bounded & Top (latt (L,I)) = Top L ) )
set b9 = the Element of (latt (L,I));
reconsider b = the Element of (latt (L,I)) as Element of L by FILTER_2:68;
assume A0: ( L is upper-bounded & Top L in I ) ; :: thesis: ( latt (L,I) is upper-bounded & Top (latt (L,I)) = Top L )
set c = Top L;
reconsider c9 = Top L as Element of (latt (L,I)) by FILTER_2:72, A0;
ex c9 being Element of (latt (L,I)) st
for a9 being Element of (latt (L,I)) holds
( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )

proof

take c9 ; :: thesis: for a9 being Element of (latt (L,I)) holds
( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
let a9 be Element of (latt (L,I)); :: thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
reconsider a = a9 as Element of L by FILTER_2:68;
thus c9 "\/" a9 = (Top L) "\/" a by FILTER_2:73
.= c9 by A0 ; :: thesis: a9 "\/" c9 = c9
hence a9 "\/" c9 = c9 ; :: thesis: verum

end;

hence W1: latt (L,I) is upper-bounded by LATTICES:def 14; :: thesis: Top (latt (L,I)) = Top L
for a9 being Element of (latt (L,I)) holds
( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )

proof

let a9 be Element of (latt (L,I)); :: thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
reconsider a = a9 as Element of L by FILTER_2:68;
thus c9 "\/" a9 = (Top L) "\/" a by FILTER_2:73
.= c9 by A0 ; :: thesis: a9 "\/" c9 = c9
hence a9 "\/" c9 = c9 ; :: thesis: verum

end;

hence Top (latt (L,I)) = Top L by LATTICES:def 17, W1; :: thesis: verum