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 A1: <.p.) = <.q.) ; :: thesis: p = q
then q in <.p.) ;
then A2: p [= q by FILTER_0:15;
p in <.q.) by A1;
then q [= p by FILTER_0:15;
hence p = q by A2, LATTICES:8; :: thesis: verum