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 )

hence field (LattRel L) = the carrier of L \/ the carrier of L by A3, RELAT_1:def 6

.= the carrier of L ;

:: thesis: verum

now :: thesis: for x being object holds

( ( x in the carrier of L implies ex y being object st [x,y] in LattRel L ) & ( ex y being object st [x,y] in LattRel L implies x in the carrier of L ) )

hence A3:
dom (LattRel L) = the carrier of L
by XTUPLE_0:def 12; :: thesis: ( rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )( ( x in the carrier of L implies ex y being object st [x,y] in LattRel L ) & ( ex y being object st [x,y] in LattRel L implies x in the carrier of L ) )

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

thus ( x in the carrier of L implies ex y being object st [x,y] in LattRel L ) :: thesis: ( ex y being object st [x,y] in LattRel L implies 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, XTUPLE_0:1;

hence x in the carrier of L ; :: thesis: verum

end;thus ( x in the carrier of L implies ex y being object st [x,y] in LattRel L ) :: thesis: ( ex y being object st [x,y] in LattRel L implies x in the carrier of L )

proof

given y being object such that A1:
[x,y] in LattRel L
; :: thesis: x in the carrier of L
assume
x in the carrier of L
; :: thesis: ex y being object st [x,y] in LattRel L

then reconsider p = x as Element of L ;

[p,p] in LattRel L ;

hence ex y being object st [x,y] in LattRel L ; :: thesis: verum

end;then reconsider p = x as Element of L ;

[p,p] in LattRel L ;

hence ex y being object st [x,y] in LattRel L ; :: thesis: verum

consider p, q being Element of L such that

A2: [x,y] = [p,q] and

p [= q by A1;

x = p by A2, XTUPLE_0:1;

hence x in the carrier of L ; :: thesis: verum

now :: thesis: for x being object holds

( ( x in the carrier of L implies ex y being object st [y,x] in LattRel L ) & ( ex y being object st [y,x] in LattRel L implies x in the carrier of L ) )

hence
rng (LattRel L) = the carrier of L
by XTUPLE_0:def 13; :: thesis: field (LattRel L) = the carrier of L( ( x in the carrier of L implies ex y being object st [y,x] in LattRel L ) & ( ex y being object st [y,x] in LattRel L implies x in the carrier of L ) )

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

thus ( x in the carrier of L implies ex y being object st [y,x] in LattRel L ) :: thesis: ( ex y being object st [y,x] in LattRel L implies 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, XTUPLE_0:1;

hence x in the carrier of L ; :: thesis: verum

end;thus ( x in the carrier of L implies ex y being object st [y,x] in LattRel L ) :: thesis: ( ex y being object st [y,x] in LattRel L implies x in the carrier of L )

proof

given y being object such that A4:
[y,x] in LattRel L
; :: thesis: x in the carrier of L
assume
x in the carrier of L
; :: thesis: ex y being object st [y,x] in LattRel L

then reconsider p = x as Element of L ;

[p,p] in LattRel L ;

hence ex y being object st [y,x] in LattRel L ; :: thesis: verum

end;then reconsider p = x as Element of L ;

[p,p] in LattRel L ;

hence ex y being object st [y,x] in LattRel L ; :: thesis: verum

consider p, q being Element of L such that

A5: [y,x] = [p,q] and

p [= q by A4;

x = q by A5, XTUPLE_0:1;

hence x in the carrier of L ; :: thesis: verum

hence field (LattRel L) = the carrier of L \/ the carrier of L by A3, RELAT_1:def 6

.= the carrier of L ;

:: thesis: verum