let L be GAD_Lattice; :: thesis: ( dom (LatOrder L) = the carrier of L & rng (LatOrder L) = the carrier of L & field (LatOrder L) = the carrier of L )
now :: thesis: for x being object holds
( ( x in the carrier of L implies ex y being object st [x,y] in LatOrder L ) & ( ex y being object st [x,y] in LatOrder 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 LatOrder L ) & ( ex y being object st [x,y] in LatOrder L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being object st [x,y] in LatOrder L ) :: thesis: ( ex y being object st [x,y] in LatOrder L implies x in the carrier of L )
proof
assume x in the carrier of L ; :: thesis: ex y being object st [x,y] in LatOrder L
then reconsider p = x as Element of L ;
p [= p by Idem;
then [p,p] in LatOrder L ;
hence ex y being object st [x,y] in LatOrder L ; :: thesis: verum
end;
given y being object such that A1: [x,y] in LatOrder 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, XTUPLE_0:1;
hence x in the carrier of L ; :: thesis: verum
end;
hence A3: dom (LatOrder L) = the carrier of L by XTUPLE_0:def 12; :: thesis: ( rng (LatOrder L) = the carrier of L & field (LatOrder L) = the carrier of L )
T1: now :: thesis: for x being object holds
( ( x in the carrier of L implies ex y being object st [y,x] in LatOrder L ) & ( ex y being object st [y,x] in LatOrder 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 LatOrder L ) & ( ex y being object st [y,x] in LatOrder L implies x in the carrier of L ) )
thus ( x in the carrier of L implies ex y being object st [y,x] in LatOrder L ) :: thesis: ( ex y being object st [y,x] in LatOrder L implies x in the carrier of L )
proof
assume x in the carrier of L ; :: thesis: ex y being object st [y,x] in LatOrder L
then reconsider p = x as Element of L ;
p [= p by Idem;
then [p,p] in LatOrder L ;
hence ex y being object st [y,x] in LatOrder L ; :: thesis: verum
end;
given y being object such that A4: [y,x] in LatOrder 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, XTUPLE_0:1;
hence x in the carrier of L ; :: thesis: verum
end;
hence rng (LatOrder L) = the carrier of L by XTUPLE_0:def 13; :: thesis: field (LatOrder L) = the carrier of L
thus field (LatOrder L) = the carrier of L \/ the carrier of L by A3, XTUPLE_0:def 13, T1
.= the carrier of L ; :: thesis: verum