A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def 8;
LattRel L c= [:H₁(L),H₁(L):]

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in LattRel L or [x,y] in [:H₁(L),H₁(L):] )
assume [x,y] in LattRel L ; :: thesis: [x,y] in [:H₁(L),H₁(L):]
then ex p, q being Element of L st
( [x,y] = [p,q] & p [= q ) by A1;
hence [x,y] in [:H₁(L),H₁(L):] by ZFMISC_1:87; :: thesis: verum

end;

then reconsider R = LattRel L as Relation of H₁(L) ;
A2: R is_reflexive_in H₁(L) by FILTER_1:31;
A3: R is_antisymmetric_in H₁(L)

proof

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in H₁(L) or not y in H₁(L) or not [x,y] in R or not [y,x] in R or x = y )
assume that
A4: x in H₁(L) and
A5: y in H₁(L) ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 = x, y9 = y as Element of L by A4, A5;
assume that
A6: [x,y] in R and
A7: [y,x] in R ; :: thesis: x = y
A8: x9 [= y9 by A6, FILTER_1:31;
y9 [= x9 by A7, FILTER_1:31;
hence x = y by A8, LATTICES:8; :: thesis: verum

end;

A9: R is_transitive_in H₁(L)

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in H₁(L) or not y in H₁(L) or not z in H₁(L) or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A10: x in H₁(L) and
A11: y in H₁(L) and
A12: z in H₁(L) ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 = x, y9 = y, z9 = z as Element of L by A10, A11, A12;
assume that
A13: [x,y] in R and
A14: [y,z] in R ; :: thesis: [x,z] in R
A15: x9 [= y9 by A13, FILTER_1:31;
y9 [= z9 by A14, FILTER_1:31;
then x9 [= z9 by A15, LATTICES:7;
hence [x,z] in R by FILTER_1:31; :: thesis: verum

end;

A16: dom R = H₁(L) by A2, ORDERS_1:13;
field R = H₁(L) by A2, ORDERS_1:13;
hence LattRel L is Order of the carrier of L by A2, A3, A9, A16, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum