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 )

( [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

thus
( p [= q implies [p,q] in LattRel L )
; :: thesis: verum
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;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