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 implies [p,q] in LattRel L ) & ( [p,q] in LattRel L implies p [= q ) & p = p % & q = q % & LattPOSet L = RelStr(# H₁(L),(LattRel L) #) ) by FILTER_1:32;
hence ( p [= q iff p % <= q % ) by ORDERS_2:def 9; :: thesis: verum