let L be finite distributive LATTICE; :: thesis: ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st

( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )

set I = InclPoset (LOWER (subrelstr (Join-IRR L)));

deffunc H_{1}( Element of L) -> Element of bool the carrier of L = (downarrow $1) /\ (Join-IRR L);

consider r being ManySortedSet of the carrier of L such that

A1: for d being Element of L holds r . d = H_{1}(d)
from PBOOLE:sch 5();

A2: rng r c= the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))

then reconsider r = r as Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) by A2, FUNCT_2:def 1, RELSET_1:4;

A12: for x, y being Element of L holds

( x <= y iff r . x <= r . y )

r is V13()

hence ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st

( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by A1; :: thesis: verum

( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )

set I = InclPoset (LOWER (subrelstr (Join-IRR L)));

deffunc H

consider r being ManySortedSet of the carrier of L such that

A1: for d being Element of L holds r . d = H

A2: rng r c= the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))

proof

dom r = the carrier of L
by PARTFUN1:def 2;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng r or t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) )

reconsider tt = t as set by TARSKI:1;

assume t in rng r ; :: thesis: t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))

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 = (downarrow x) /\ (Join-IRR L) by A1, A4;

then tt c= Join-IRR L by XBOOLE_1:17;

then reconsider t = t as Subset of (subrelstr (Join-IRR L)) by YELLOW_0:def 15;

A6: t is lower

hence t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) by A6; :: thesis: verum

end;reconsider tt = t as set by TARSKI:1;

assume t in rng r ; :: thesis: t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))

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 = (downarrow x) /\ (Join-IRR L) by A1, A4;

then tt c= Join-IRR L by XBOOLE_1:17;

then reconsider t = t as Subset of (subrelstr (Join-IRR L)) by YELLOW_0:def 15;

A6: t is lower

proof

the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) = LOWER (subrelstr (Join-IRR L))
by YELLOW_1:1;
let c, d be Element of (subrelstr (Join-IRR L)); :: 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 A5, A7, XBOOLE_0:def 4;

then A11: c1 <= x by WAYBEL_0:17;

d1 <= c1 by A8, YELLOW_0:59;

then d1 <= x by A11, ORDERS_2:3;

then d1 in downarrow x by WAYBEL_0:17;

hence d in t by A5, A10, A9, XBOOLE_0:def 4; :: thesis: verum

end;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 A5, A7, XBOOLE_0:def 4;

then A11: c1 <= x by WAYBEL_0:17;

d1 <= c1 by A8, YELLOW_0:59;

then d1 <= x by A11, ORDERS_2:3;

then d1 in downarrow x by WAYBEL_0:17;

hence d in t by A5, A10, A9, XBOOLE_0:def 4; :: thesis: verum

hence t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) by A6; :: thesis: verum

then reconsider r = r as Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) by A2, FUNCT_2:def 1, RELSET_1:4;

A12: for x, y being Element of L holds

( x <= y iff r . x <= r . y )

proof

the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) c= rng r
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 )

end;thus ( x <= y implies r . x <= r . y ) :: thesis: ( r . x <= r . y implies x <= y )

proof

thus
( r . x <= r . y implies x <= y )
:: thesis: verum
assume A13:
x <= y
; :: thesis: r . x <= r . y

(downarrow x) /\ (Join-IRR L) c= (downarrow y) /\ (Join-IRR L)

then r . x c= r . y by A1;

hence r . x <= r . y by YELLOW_1:3; :: thesis: verum

end;(downarrow x) /\ (Join-IRR L) c= (downarrow y) /\ (Join-IRR L)

proof

then
r . x c= (downarrow y) /\ (Join-IRR L)
by A1;
let a be Element of L; :: according to LATTICE7:def 1 :: thesis: ( a in (downarrow x) /\ (Join-IRR L) implies a in (downarrow y) /\ (Join-IRR L) )

assume a in (downarrow x) /\ (Join-IRR L) ; :: thesis: a in (downarrow y) /\ (Join-IRR L)

then A14: ( a in downarrow x & a in Join-IRR L ) by XBOOLE_0:def 4;

downarrow x c= downarrow y by A13, WAYBEL_0:21;

hence a in (downarrow y) /\ (Join-IRR L) by A14, XBOOLE_0:def 4; :: thesis: verum

end;assume a in (downarrow x) /\ (Join-IRR L) ; :: thesis: a in (downarrow y) /\ (Join-IRR L)

then A14: ( a in downarrow x & a in Join-IRR L ) by XBOOLE_0:def 4;

downarrow x c= downarrow y by A13, WAYBEL_0:21;

hence a in (downarrow y) /\ (Join-IRR L) by A14, XBOOLE_0:def 4; :: thesis: verum

then r . x c= r . y by A1;

hence r . x <= r . y by YELLOW_1:3; :: thesis: verum

proof

( r . x = (downarrow x) /\ (Join-IRR L) & r . y = (downarrow y) /\ (Join-IRR L) )
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 A15, YELLOW_0:34;

then sup ((downarrow x) /\ (Join-IRR L)) <= sup ry by A1;

then sup ((downarrow x) /\ (Join-IRR L)) <= sup ((downarrow y) /\ (Join-IRR L)) by A1;

then x <= sup ((downarrow y) /\ (Join-IRR L)) by Th12;

hence x <= y by Th12; :: thesis: verum

end;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 A15, YELLOW_0:34;

then sup ((downarrow x) /\ (Join-IRR L)) <= sup ry by A1;

then sup ((downarrow x) /\ (Join-IRR L)) <= sup ((downarrow y) /\ (Join-IRR L)) by A1;

then x <= sup ((downarrow y) /\ (Join-IRR L)) by Th12;

hence x <= y by Th12; :: thesis: verum

proof

then A36:
rng r = the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
by XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) or x in rng r )

assume A16: x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) ; :: thesis: x in rng r

thus x in rng r :: thesis: verum

end;assume A16: x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) ; :: thesis: x in rng r

thus x in rng r :: thesis: verum

proof

x in LOWER (subrelstr (Join-IRR L))
by A16, YELLOW_1:1;

then consider X being Subset of (subrelstr (Join-IRR L)) such that

A17: x = X and

A18: X is lower ;

the carrier of (subrelstr (Join-IRR L)) c= Join-IRR L by YELLOW_0:def 15;

then the carrier of (subrelstr (Join-IRR L)) 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 )

end;then consider X being Subset of (subrelstr (Join-IRR L)) such that

A17: x = X and

A18: X is lower ;

the carrier of (subrelstr (Join-IRR L)) c= Join-IRR L by YELLOW_0:def 15;

then the carrier of (subrelstr (Join-IRR L)) 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

hence
x in rng r
by FUNCT_1:def 3; :: thesis: verum
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)) /\ (Join-IRR L) c= X1

hence x = r . y by A1, A17; :: thesis: verum

end;dom r = the carrier of L by FUNCT_2:def 1;

hence y in dom r ; :: thesis: x = r . y

A19: (downarrow (sup X1)) /\ (Join-IRR L) c= X1

proof

X1 c= (downarrow (sup X1)) /\ (Join-IRR L)
let r be Element of L; :: according to LATTICE7:def 1 :: thesis: ( r in (downarrow (sup X1)) /\ (Join-IRR L) implies r in X1 )

reconsider r1 = r as Element of L ;

assume A20: r in (downarrow (sup X1)) /\ (Join-IRR L) ; :: thesis: r in X1

then r in downarrow (sup X1) by XBOOLE_0:def 4;

then A21: r1 <= sup X1 by WAYBEL_0:17;

end;reconsider r1 = r as Element of L ;

assume A20: r in (downarrow (sup X1)) /\ (Join-IRR L) ; :: 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 )
;

end;

suppose A22:
not r1 in X1
; :: thesis: r in X1

A23:
r1 in Join-IRR L
by A20, XBOOLE_0:def 4;

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

( r1 = r1 "/\" (sup X1) & r1 "/\" (sup X1) = sup ({r1} "/\" X1) ) by A21, WAYBEL_2:15, YELLOW_0:25;

hence r in X1 by A24, A32, ORDERS_2:7; :: thesis: verum

end;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

then A32:
sup ({r1} "/\" X1) <= z
by YELLOW_0:32;
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 (subrelstr (Join-IRR L)) by A23, YELLOW_0:def 15;

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 (subrelstr (Join-IRR L)) by A23, A28, YELLOW_0:def 15;

A29: ex_inf_of {r1,x},L by YELLOW_0:17;

then A30: a <= x by A27, YELLOW_0:19;

A31: a <> r1 by A18, A22, A28, A30, A26, YELLOW_0:60;

a <= r1 by A27, A29, YELLOW_0:19;

then a < r1 by A31, ORDERS_2:def 6;

hence a <= z by A25; :: thesis: verum

end;A26: r1 in the carrier of (subrelstr (Join-IRR L)) by A23, YELLOW_0:def 15;

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 (subrelstr (Join-IRR L)) by A23, A28, YELLOW_0:def 15;

A29: ex_inf_of {r1,x},L by YELLOW_0:17;

then A30: a <= x by A27, YELLOW_0:19;

A31: a <> r1 by A18, A22, A28, A30, A26, YELLOW_0:60;

a <= r1 by A27, A29, YELLOW_0:19;

then a < r1 by A31, ORDERS_2:def 6;

hence a <= z by A25; :: thesis: verum

( r1 = r1 "/\" (sup X1) & r1 "/\" (sup X1) = sup ({r1} "/\" X1) ) by A21, WAYBEL_2:15, YELLOW_0:25;

hence r in X1 by A24, A32, ORDERS_2:7; :: thesis: verum

proof

then
X1 = (downarrow (sup X1)) /\ (Join-IRR L)
by A19, XBOOLE_0:def 10;
let a be Element of L; :: according to LATTICE7:def 1 :: thesis: ( a in X1 implies a in (downarrow (sup X1)) /\ (Join-IRR L) )

assume A33: a in X1 ; :: thesis: a in (downarrow (sup X1)) /\ (Join-IRR L)

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 )

X is Subset of (Join-IRR L) by YELLOW_0:def 15;

hence a in (downarrow (sup X1)) /\ (Join-IRR L) by A33, A35, XBOOLE_0:def 4; :: thesis: verum

end;assume A33: a in X1 ; :: thesis: a in (downarrow (sup X1)) /\ (Join-IRR L)

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

then A35:
a in downarrow {(sup X1)}
by WAYBEL_0:def 15;
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 A33, A34; :: thesis: verum

end;thus y in {(sup X1)} by TARSKI:def 1; :: thesis: a <= y

thus a <= y by A33, A34; :: thesis: verum

X is Subset of (Join-IRR L) by YELLOW_0:def 15;

hence a in (downarrow (sup X1)) /\ (Join-IRR L) by A33, A35, XBOOLE_0:def 4; :: thesis: verum

hence x = r . y by A1, A17; :: thesis: verum

r is V13()

proof

then
r is isomorphic
by A36, A12, WAYBEL_0:66;
let x, y be Element of L; :: according to WAYBEL_1:def 1 :: thesis: ( not r . x = r . y or x = y )

r . y = (downarrow y) /\ (Join-IRR L) by A1;

then reconsider ry = r . y as Subset of L ;

assume r . x = r . y ; :: thesis: x = y

then sup ((downarrow x) /\ (Join-IRR L)) = sup ry by A1;

then sup ((downarrow x) /\ (Join-IRR L)) = sup ((downarrow y) /\ (Join-IRR L)) by A1;

then x = sup ((downarrow y) /\ (Join-IRR L)) by Th12;

hence x = y by Th12; :: thesis: verum

end;r . y = (downarrow y) /\ (Join-IRR L) by A1;

then reconsider ry = r . y as Subset of L ;

assume r . x = r . y ; :: thesis: x = y

then sup ((downarrow x) /\ (Join-IRR L)) = sup ry by A1;

then sup ((downarrow x) /\ (Join-IRR L)) = sup ((downarrow y) /\ (Join-IRR L)) by A1;

then x = sup ((downarrow y) /\ (Join-IRR L)) by Th12;

hence x = y by Th12; :: thesis: verum

hence ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st

( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by A1; :: thesis: verum