let L be Lattice; :: thesis: for p, q being Element of L st p [= q holds
( latt L,[#p,q#] is bounded & Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p )
let p, q be Element of L; :: thesis: ( p [= q implies ( latt L,[#p,q#] is bounded & Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p ) )
assume A1: p [= q ; :: thesis: ( latt L,[#p,q#] is bounded & Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p )
A2: H₁( latt L,[#p,q#]) = [#p,q#] by Th73;
then reconsider p' = p, q' = q as Element of (latt L,[#p,q#]) by A1, Th63;

A3: now

let a' be Element of (latt L,[#p,q#]); :: thesis: ( p' "/\" a' = p' & a' "/\" p' = p' )
reconsider a = a' as Element of L by Th69;
A4: p [= a by A1, A2, Th63;
thus p' "/\" a' = p "/\" a by Th74
.= p' by A4, LATTICES:21 ; :: thesis: a' "/\" p' = p'
hence a' "/\" p' = p' ; :: thesis: verum

end;

A5: now

let a' be Element of (latt L,[#p,q#]); :: thesis: ( q' "\/" a' = q' & a' "\/" q' = q' )
reconsider a = a' as Element of L by Th69;
A6: a [= q by A1, A2, Th63;
thus q' "\/" a' = q "\/" a by Th74
.= q' by A6, LATTICES:def 3 ; :: thesis: a' "\/" q' = q'
hence a' "\/" q' = q' ; :: thesis: verum

end;

then A7: latt L,[#p,q#] is lower-bounded upper-bounded Lattice by A3, LATTICES:def 13, LATTICES:def 14;
hence latt L,[#p,q#] is bounded ; :: thesis: ( Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p )
thus ( Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p ) by A3, A5, A7, LATTICES:def 16, LATTICES:def 17; :: thesis: verum