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

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