A1: LattRel L = { [p,q] where p, q is Element of : p [= q } by FILTER_1:def 8;
LattRel L c= [:the carrier of L,the carrier of L:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LattRel L or x in [:the carrier of L,the carrier of L:] )
assume x in LattRel L ; :: thesis: x in [:the carrier of L,the carrier of L:]
then ex p, q being Element of st
( x = [p,q] & p [= q ) by A1;
hence x in [:the carrier of L,the carrier of L:] by ZFMISC_1:106; :: thesis: verum

end;

then reconsider R = LattRel L as Relation of ;
A2: R is_antisymmetric_in the carrier of L

proof

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in R or not [y,x] in R or x = y )
assume ( x in the carrier of L & y in the carrier of 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 ;
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;

A3: R is_transitive_in the carrier of L

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume ( x in the carrier of L & y in the carrier of L & z in the carrier of 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 ;
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;

A4: R is_reflexive_in the carrier of L

proof

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

end;

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