let L be Lattice; :: thesis: ( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )

now

let x be set ; :: thesis: ( ( x in the carrier of L implies ex y being set st [x,y] in LattRel L ) & ( ex y being set st [x,y] in LattRel L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being set st [x,y] in LattRel L ) :: thesis: ( ex y being set st [x,y] in LattRel L implies x in the carrier of L )

proof

assume x in the carrier of L ; :: thesis: ex y being set st [x,y] in LattRel L
then reconsider p = x as Element of L ;
[p,p] in LattRel L ;
hence ex y being set st [x,y] in LattRel L ; :: thesis: verum

end;

given y being set such that A1: [x,y] in LattRel L ; :: thesis: x in the carrier of L
consider p, q being Element of L such that
A2: [x,y] = [p,q] and
p [= q by A1;
x = p by A2, ZFMISC_1:33;
hence x in the carrier of L ; :: thesis: verum

end;

hence A3: dom (LattRel L) = the carrier of L by RELAT_1:def 4; :: thesis: ( rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )

now

let x be set ; :: thesis: ( ( x in the carrier of L implies ex y being set st [y,x] in LattRel L ) & ( ex y being set st [y,x] in LattRel L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being set st [y,x] in LattRel L ) :: thesis: ( ex y being set st [y,x] in LattRel L implies x in the carrier of L )

proof

assume x in the carrier of L ; :: thesis: ex y being set st [y,x] in LattRel L
then reconsider p = x as Element of L ;
[p,p] in LattRel L ;
hence ex y being set st [y,x] in LattRel L ; :: thesis: verum

end;

given y being set such that A4: [y,x] in LattRel L ; :: thesis: x in the carrier of L
consider p, q being Element of L such that
A5: [y,x] = [p,q] and
p [= q by A4;
x = q by A5, ZFMISC_1:33;
hence x in the carrier of L ; :: thesis: verum

end;

hence rng (LattRel L) = the carrier of L by RELAT_1:def 5; :: thesis: field (LattRel L) = the carrier of L
hence field (LattRel L) = the carrier of L \/ the carrier of L by A3, RELAT_1:def 6
.= the carrier of L ;
:: thesis: verum