A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def 8;
LattRel L c= [: the carrier of L, the carrier of L:]
proof
let x be object ; :: 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 L st
( x = [p,q] & p [= q ) by A1;
hence x in [: the carrier of L, the carrier of L:] by ZFMISC_1:87; :: thesis: verum
end;
then reconsider R = LattRel L as Relation of the carrier of L ;
A2: R is_antisymmetric_in the carrier of L
proof
let x, y be object ; :: 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 x9 = x, y9 = y as Element of L ;
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x9 [= y9 & y9 [= x9 ) by FILTER_1:31;
hence x = y by LATTICES:8; :: thesis: verum
end;
A3: R is_transitive_in the carrier of L
proof
let x, y, z be object ; :: 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 x9 = x, y9 = y, z9 = z as Element of L ;
assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( x9 [= y9 & y9 [= z9 ) by FILTER_1:31;
then x9 [= z9 by LATTICES:7;
hence [x,z] in R by FILTER_1:31; :: thesis: verum
end;
A4: R is_reflexive_in the carrier of L by FILTER_1:31;
then ( dom R = the carrier of L & field R = the carrier of L ) by ORDERS_1:13;
hence LattRel L is Order of the carrier of L by A4, A2, A3, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum