let L be Lattice; :: thesis: for p, q being Element of L st <.p.) = <.q.) holds
p = q
let p, q be Element of L; :: thesis: ( <.p.) = <.q.) implies p = q )
assume <.p.) = <.q.) ; :: thesis: p = q
then ( p in <.q.) & q in <.p.) ) ;
then ( p [= q & q [= p ) by FILTER_0:18;
hence p = q by LATTICES:26; :: thesis: verum