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