let L be Lattice; :: thesis: for p, q being Element of L holds
( p [= q iff p % <= q % )
let p, q be Element of L; :: thesis: ( p [= q iff p % <= q % )
( p [= q iff [p,q] in LattRel L ) by FILTER_1:31;
hence ( p [= q iff p % <= q % ) by ORDERS_2:def 5; :: thesis: verum