let L be Lattice; :: thesis: for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )
let I be Ideal of L; :: thesis: ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) )
(.I.> = I by Th37;
hence ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) ) by Th41; :: thesis: verum