let L be finite distributive LATTICE; :: thesis: ex r being Function of L,(InclPoset (LOWER ())) st
( r is isomorphic & ( for a being Element of L holds r . a = () /\ () ) )

set I = InclPoset (LOWER ());
deffunc H1( Element of L) -> Element of bool the carrier of L = () /\ ();
consider r being ManySortedSet of the carrier of L such that
A1: for d being Element of L holds r . d = H1(d) from PBOOLE:sch 5();
A2: rng r c= the carrier of (InclPoset (LOWER ()))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng r or t in the carrier of (InclPoset (LOWER ())) )
reconsider tt = t as set by TARSKI:1;
assume t in rng r ; :: thesis: t in the carrier of (InclPoset (LOWER ()))
then consider x being object such that
A3: x in dom r and
A4: t = r . x by FUNCT_1:def 3;
reconsider x = x as Element of L by A3;
A5: t = () /\ () by A1, A4;
then tt c= Join-IRR L by XBOOLE_1:17;
then reconsider t = t as Subset of () by YELLOW_0:def 15;
A6: t is lower
proof
let c, d be Element of (); :: according to WAYBEL_0:def 19 :: thesis: ( not c in t or not d <= c or d in t )
assume that
A7: c in t and
A8: d <= c ; :: thesis: d in t
A9: d is Element of Join-IRR L by YELLOW_0:def 15;
A10: not Join-IRR L is empty by A5, A7;
then d in Join-IRR L by A9;
then reconsider c1 = c, d1 = d as Element of L by A5, A7;
c in downarrow x by ;
then A11: c1 <= x by WAYBEL_0:17;
d1 <= c1 by ;
then d1 <= x by ;
then d1 in downarrow x by WAYBEL_0:17;
hence d in t by ; :: thesis: verum
end;
the carrier of (InclPoset (LOWER ())) = LOWER () by YELLOW_1:1;
hence t in the carrier of (InclPoset (LOWER ())) by A6; :: thesis: verum
end;
dom r = the carrier of L by PARTFUN1:def 2;
then reconsider r = r as Function of L,(InclPoset (LOWER ())) by ;
A12: for x, y being Element of L holds
( x <= y iff r . x <= r . y )
proof
let x, y be Element of L; :: thesis: ( x <= y iff r . x <= r . y )
thus ( x <= y implies r . x <= r . y ) :: thesis: ( r . x <= r . y implies x <= y )
proof
assume A13: x <= y ; :: thesis: r . x <= r . y
(downarrow x) /\ () c= () /\ ()
proof
let a be Element of L; :: according to LATTICE7:def 1 :: thesis: ( a in () /\ () implies a in () /\ () )
assume a in () /\ () ; :: thesis: a in () /\ ()
then A14: ( a in downarrow x & a in Join-IRR L ) by XBOOLE_0:def 4;
downarrow x c= downarrow y by ;
hence a in () /\ () by ; :: thesis: verum
end;
then r . x c= () /\ () by A1;
then r . x c= r . y by A1;
hence r . x <= r . y by YELLOW_1:3; :: thesis: verum
end;
thus ( r . x <= r . y implies x <= y ) :: thesis: verum
proof
( r . x = () /\ () & r . y = () /\ () ) by A1;
then reconsider rx = r . x, ry = r . y as Subset of L ;
assume r . x <= r . y ; :: thesis: x <= y
then A15: rx c= ry by YELLOW_1:3;
( ex_sup_of rx,L & ex_sup_of ry,L ) by YELLOW_0:17;
then sup rx <= sup ry by ;
then sup (() /\ ()) <= sup ry by A1;
then sup (() /\ ()) <= sup (() /\ ()) by A1;
then x <= sup (() /\ ()) by Th12;
hence x <= y by Th12; :: thesis: verum
end;
end;
the carrier of (InclPoset (LOWER ())) c= rng r
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (InclPoset (LOWER ())) or x in rng r )
assume A16: x in the carrier of (InclPoset (LOWER ())) ; :: thesis: x in rng r
thus x in rng r :: thesis: verum
proof
x in LOWER () by ;
then consider X being Subset of () such that
A17: x = X and
A18: X is lower ;
the carrier of () c= Join-IRR L by YELLOW_0:def 15;
then the carrier of () c= the carrier of L by XBOOLE_1:1;
then reconsider X1 = X as Subset of L by XBOOLE_1:1;
ex y being set st
( y in dom r & x = r . y )
proof
take y = sup X1; :: thesis: ( y in dom r & x = r . y )
dom r = the carrier of L by FUNCT_2:def 1;
hence y in dom r ; :: thesis: x = r . y
A19: (downarrow (sup X1)) /\ () c= X1
proof
let r be Element of L; :: according to LATTICE7:def 1 :: thesis: ( r in (downarrow (sup X1)) /\ () implies r in X1 )
reconsider r1 = r as Element of L ;
assume A20: r in (downarrow (sup X1)) /\ () ; :: thesis: r in X1
then r in downarrow (sup X1) by XBOOLE_0:def 4;
then A21: r1 <= sup X1 by WAYBEL_0:17;
per cases ( r1 in X1 or not r1 in X1 ) ;
suppose r1 in X1 ; :: thesis: r in X1
hence r in X1 ; :: thesis: verum
end;
suppose A22: not r1 in X1 ; :: thesis: r in X1
A23: r1 in Join-IRR L by ;
then consider z being Element of L such that
A24: z < r1 and
A25: for y being Element of L st y < r1 holds
y <= z by Th11;
{r1} "/\" X1 is_<=_than z
proof
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in {r1} "/\" X1 or a <= z )
A26: r1 in the carrier of () by ;
assume a in {r1} "/\" X1 ; :: thesis: a <= z
then a in { (r1 "/\" k) where k is Element of L : k in X1 } by YELLOW_4:42;
then consider x being Element of L such that
A27: a = r1 "/\" x and
A28: x in X1 ;
reconsider r9 = r1, x9 = x as Element of () by ;
A29: ex_inf_of {r1,x},L by YELLOW_0:17;
then A30: a <= x by ;
A31: a <> r1 by ;
a <= r1 by ;
then a < r1 by ;
hence a <= z by A25; :: thesis: verum
end;
then A32: sup ({r1} "/\" X1) <= z by YELLOW_0:32;
( r1 = r1 "/\" (sup X1) & r1 "/\" (sup X1) = sup ({r1} "/\" X1) ) by ;
hence r in X1 by ; :: thesis: verum
end;
end;
end;
X1 c= (downarrow (sup X1)) /\ ()
proof
let a be Element of L; :: according to LATTICE7:def 1 :: thesis: ( a in X1 implies a in (downarrow (sup X1)) /\ () )
assume A33: a in X1 ; :: thesis: a in (downarrow (sup X1)) /\ ()
set A = a;
ex_sup_of X1,L by YELLOW_0:17;
then A34: X1 is_<=_than "\/" (X1,L) by YELLOW_0:def 9;
ex y being Element of L st
( y in {(sup X1)} & a <= y )
proof
take y = sup X1; :: thesis: ( y in {(sup X1)} & a <= y )
thus y in {(sup X1)} by TARSKI:def 1; :: thesis: a <= y
thus a <= y by ; :: thesis: verum
end;
then A35: a in downarrow {(sup X1)} by WAYBEL_0:def 15;
X is Subset of () by YELLOW_0:def 15;
hence a in (downarrow (sup X1)) /\ () by ; :: thesis: verum
end;
then X1 = (downarrow (sup X1)) /\ () by ;
hence x = r . y by ; :: thesis: verum
end;
hence x in rng r by FUNCT_1:def 3; :: thesis: verum
end;
end;
then A36: rng r = the carrier of (InclPoset (LOWER ())) by XBOOLE_0:def 10;
r is V13()
proof
let x, y be Element of L; :: according to WAYBEL_1:def 1 :: thesis: ( not r . x = r . y or x = y )
r . y = () /\ () by A1;
then reconsider ry = r . y as Subset of L ;
assume r . x = r . y ; :: thesis: x = y
then sup (() /\ ()) = sup ry by A1;
then sup (() /\ ()) = sup (() /\ ()) by A1;
then x = sup (() /\ ()) by Th12;
hence x = y by Th12; :: thesis: verum
end;
then r is isomorphic by ;
hence ex r being Function of L,(InclPoset (LOWER ())) st
( r is isomorphic & ( for a being Element of L holds r . a = () /\ () ) ) by A1; :: thesis: verum