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 Th72;
then reconsider p9 = p, q9 = q as Element of (latt (L,[#p,q#])) by A1, Th62;

A3: now :: thesis: for a9 being Element of (latt (L,[#p,q#])) holds
( q9 "\/" a9 = q9 & a9 "\/" q9 = q9 )

let a9 be Element of (latt (L,[#p,q#])); :: thesis: ( q9 "\/" a9 = q9 & a9 "\/" q9 = q9 )
reconsider a = a9 as Element of L by Th68;
A4: a [= q by A1, A2, Th62;
thus q9 "\/" a9 = q "\/" a by Th73
.= q9 by A4 ; :: thesis: a9 "\/" q9 = q9
hence a9 "\/" q9 = q9 ; :: thesis: verum

end;

A5: now :: thesis: for a9 being Element of (latt (L,[#p,q#])) holds
( p9 "/\" a9 = p9 & a9 "/\" p9 = p9 )

let a9 be Element of (latt (L,[#p,q#])); :: thesis: ( p9 "/\" a9 = p9 & a9 "/\" p9 = p9 )
reconsider a = a9 as Element of L by Th68;
A6: p [= a by A1, A2, Th62;
thus p9 "/\" a9 = p "/\" a by Th73
.= p9 by A6, LATTICES:4 ; :: thesis: a9 "/\" p9 = p9
hence a9 "/\" p9 = p9 ; :: 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 A5, A3, A7, LATTICES:def 16, LATTICES:def 17; :: thesis: verum