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 set ; :: 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:106; :: thesis: verum

end;

then reconsider R = LattRel L as Relation of H₁(L) ;
A2: R is_reflexive_in H₁(L)

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in H₁(L) or [x,x] in R )
assume x in H₁(L) ; :: thesis: [x,x] in R
then reconsider x = x as Element of L ;
x [= x ;
hence [x,x] in R by FILTER_1:32; :: thesis: verum

end;

A3: R is_antisymmetric_in H₁(L)

proof

let x, y be set ; :: 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 ( x in H₁(L) & y in H₁(L) ) ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
then reconsider x' = x, y' = y as Element of L ;
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x' [= y' & y' [= x' ) by FILTER_1:32;
hence x = y by LATTICES:26; :: thesis: verum

end;

A4: R is_transitive_in H₁(L)

proof

let x, y, z be set ; :: 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 ( x in H₁(L) & y in H₁(L) & z in H₁(L) ) ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
then reconsider x' = x, y' = y, z' = z as Element of L ;
assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( x' [= y' & y' [= z' ) by FILTER_1:32;
then x' [= z' by LATTICES:25;
hence [x,z] in R by FILTER_1:32; :: thesis: verum

end;

A5: dom R = H₁(L) by A2, ORDERS_1:98;
field R = H₁(L) by A2, ORDERS_1:98;
hence LattRel L is Order of the carrier of L by A2, A3, A4, A5, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum