let L be Lattice; :: thesis: for p, q being Element of L holds
( [p,q] in LattRel L iff p [= q )
let p, q be Element of L; :: thesis: ( [p,q] in LattRel L iff p [= q )
thus ( [p,q] in LattRel L implies p [= q ) :: thesis: ( p [= q implies [p,q] in LattRel L )

proof

assume [p,q] in LattRel L ; :: thesis: p [= q
then consider r, s being Element of L such that
A1: [p,q] = [r,s] and
A2: r [= s ;
thus p [= q by A1, A2, XTUPLE_0:1; :: thesis: verum

end;

thus ( p [= q implies [p,q] in LattRel L ) ; :: thesis: verum