let L be finite distributive LATTICE; :: thesis: for a being Element of L st ( for b being Element of L st b < a holds

sup ((downarrow b) /\ (Join-IRR L)) = b ) holds

sup ((downarrow a) /\ (Join-IRR L)) = a

let a be Element of L; :: thesis: ( ( for b being Element of L st b < a holds

sup ((downarrow b) /\ (Join-IRR L)) = b ) implies sup ((downarrow a) /\ (Join-IRR L)) = a )

assume A1: for b being Element of L st b < a holds

sup ((downarrow b) /\ (Join-IRR L)) = b ; :: thesis: sup ((downarrow a) /\ (Join-IRR L)) = a

thus sup ((downarrow a) /\ (Join-IRR L)) = a :: thesis: verum

sup ((downarrow b) /\ (Join-IRR L)) = b ) holds

sup ((downarrow a) /\ (Join-IRR L)) = a

let a be Element of L; :: thesis: ( ( for b being Element of L st b < a holds

sup ((downarrow b) /\ (Join-IRR L)) = b ) implies sup ((downarrow a) /\ (Join-IRR L)) = a )

assume A1: for b being Element of L st b < a holds

sup ((downarrow b) /\ (Join-IRR L)) = b ; :: thesis: sup ((downarrow a) /\ (Join-IRR L)) = a

thus sup ((downarrow a) /\ (Join-IRR L)) = a :: thesis: verum

proof
end;

per cases
( a = Bottom L or ( not a in Join-IRR L & a <> Bottom L ) or a in Join-IRR L )
;

end;

suppose A2:
a = Bottom L
; :: thesis: sup ((downarrow a) /\ (Join-IRR L)) = a

A3:
{(Bottom L)} /\ (Join-IRR L) = {}

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A2, A3, YELLOW_0:def 11; :: thesis: verum

end;proof

downarrow a = {(Bottom L)}
by A2, WAYBEL_4:23;
set x = the Element of {(Bottom L)} /\ (Join-IRR L);

assume A4: {(Bottom L)} /\ (Join-IRR L) <> {} ; :: thesis: contradiction

then the Element of {(Bottom L)} /\ (Join-IRR L) in {(Bottom L)} by XBOOLE_0:def 4;

then A5: the Element of {(Bottom L)} /\ (Join-IRR L) = Bottom L by TARSKI:def 1;

the Element of {(Bottom L)} /\ (Join-IRR L) in Join-IRR L by A4, XBOOLE_0:def 4;

hence contradiction by A5, Th10; :: thesis: verum

end;assume A4: {(Bottom L)} /\ (Join-IRR L) <> {} ; :: thesis: contradiction

then the Element of {(Bottom L)} /\ (Join-IRR L) in {(Bottom L)} by XBOOLE_0:def 4;

then A5: the Element of {(Bottom L)} /\ (Join-IRR L) = Bottom L by TARSKI:def 1;

the Element of {(Bottom L)} /\ (Join-IRR L) in Join-IRR L by A4, XBOOLE_0:def 4;

hence contradiction by A5, Th10; :: thesis: verum

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A2, A3, YELLOW_0:def 11; :: thesis: verum

suppose
( not a in Join-IRR L & a <> Bottom L )
; :: thesis: sup ((downarrow a) /\ (Join-IRR L)) = a

then consider y, z being Element of L such that

A6: a = y "\/" z and

A7: a <> y and

A8: a <> z ;

A9: y <= a by A6, YELLOW_0:22;

then A10: y < a by A7, ORDERS_2:def 6;

A11: (downarrow a) /\ (Join-IRR L) c= ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L))

A16: ex_sup_of (downarrow z) /\ (Join-IRR L),L by YELLOW_0:17;

A17: z <= a by A6, YELLOW_0:22;

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

then sup ((downarrow a) /\ (Join-IRR L)) = (sup ((downarrow y) /\ (Join-IRR L))) "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A15, A16, YELLOW_0:36;

then A19: sup ((downarrow a) /\ (Join-IRR L)) = y "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A1, A10;

z < a by A8, A17, ORDERS_2:def 6;

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A1, A6, A19; :: thesis: verum

end;A6: a = y "\/" z and

A7: a <> y and

A8: a <> z ;

A9: y <= a by A6, YELLOW_0:22;

then A10: y < a by A7, ORDERS_2:def 6;

A11: (downarrow a) /\ (Join-IRR L) c= ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L))

proof

A15:
( ex_sup_of ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)),L & ex_sup_of (downarrow y) /\ (Join-IRR L),L )
by YELLOW_0:17;
let x be Element of L; :: according to LATTICE7:def 1 :: thesis: ( x in (downarrow a) /\ (Join-IRR L) implies x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) )

set x1 = x;

set y1 = y;

set a1 = a;

set z1 = z;

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

then A13: x in Join-IRR L by XBOOLE_0:def 4;

x in downarrow a by A12, XBOOLE_0:def 4;

then A14: x <= a by WAYBEL_0:17;

x "/\" a = (x "/\" y) "\/" (x "/\" z) by A6, WAYBEL_1:def 3;

then x = (x "/\" y) "\/" (x "/\" z) by A14, YELLOW_0:25;

then ( x = x "/\" y or x = x "/\" z ) by A13, Th10;

then ( x <= y or x <= z ) by YELLOW_0:25;

then ( x in downarrow y or x in downarrow z ) by WAYBEL_0:17;

then ( x in (downarrow y) /\ (Join-IRR L) or x in (downarrow z) /\ (Join-IRR L) ) by A13, XBOOLE_0:def 4;

hence x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) by XBOOLE_0:def 3; :: thesis: verum

end;set x1 = x;

set y1 = y;

set a1 = a;

set z1 = z;

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

then A13: x in Join-IRR L by XBOOLE_0:def 4;

x in downarrow a by A12, XBOOLE_0:def 4;

then A14: x <= a by WAYBEL_0:17;

x "/\" a = (x "/\" y) "\/" (x "/\" z) by A6, WAYBEL_1:def 3;

then x = (x "/\" y) "\/" (x "/\" z) by A14, YELLOW_0:25;

then ( x = x "/\" y or x = x "/\" z ) by A13, Th10;

then ( x <= y or x <= z ) by YELLOW_0:25;

then ( x in downarrow y or x in downarrow z ) by WAYBEL_0:17;

then ( x in (downarrow y) /\ (Join-IRR L) or x in (downarrow z) /\ (Join-IRR L) ) by A13, XBOOLE_0:def 4;

hence x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) by XBOOLE_0:def 3; :: thesis: verum

A16: ex_sup_of (downarrow z) /\ (Join-IRR L),L by YELLOW_0:17;

A17: z <= a by A6, YELLOW_0:22;

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

proof

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

( (downarrow y) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) & (downarrow z) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) ) by A9, A17, WAYBEL_0:21, XBOOLE_1:26;

then A18: ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) c= (downarrow a) /\ (Join-IRR L) by XBOOLE_1:8;

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

hence x in (downarrow a) /\ (Join-IRR L) by A18; :: thesis: verum

end;( (downarrow y) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) & (downarrow z) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) ) by A9, A17, WAYBEL_0:21, XBOOLE_1:26;

then A18: ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) c= (downarrow a) /\ (Join-IRR L) by XBOOLE_1:8;

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

hence x in (downarrow a) /\ (Join-IRR L) by A18; :: thesis: verum

then sup ((downarrow a) /\ (Join-IRR L)) = (sup ((downarrow y) /\ (Join-IRR L))) "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A15, A16, YELLOW_0:36;

then A19: sup ((downarrow a) /\ (Join-IRR L)) = y "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A1, A10;

z < a by A8, A17, ORDERS_2:def 6;

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A1, A6, A19; :: thesis: verum

suppose A20:
a in Join-IRR L
; :: thesis: sup ((downarrow a) /\ (Join-IRR L)) = a

a <= a
;

then a in downarrow a by WAYBEL_0:17;

then a in (downarrow a) /\ (Join-IRR L) by A20, XBOOLE_0:def 4;

then A21: a <= sup ((downarrow a) /\ (Join-IRR L)) by YELLOW_0:17, YELLOW_4:1;

( ex_sup_of (downarrow a) /\ (Join-IRR L),L & ex_sup_of downarrow a,L ) by YELLOW_0:17;

then sup ((downarrow a) /\ (Join-IRR L)) <= sup (downarrow a) by XBOOLE_1:17, YELLOW_0:34;

then sup ((downarrow a) /\ (Join-IRR L)) <= a by WAYBEL_0:34;

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A21, ORDERS_2:2; :: thesis: verum

end;then a in downarrow a by WAYBEL_0:17;

then a in (downarrow a) /\ (Join-IRR L) by A20, XBOOLE_0:def 4;

then A21: a <= sup ((downarrow a) /\ (Join-IRR L)) by YELLOW_0:17, YELLOW_4:1;

( ex_sup_of (downarrow a) /\ (Join-IRR L),L & ex_sup_of downarrow a,L ) by YELLOW_0:17;

then sup ((downarrow a) /\ (Join-IRR L)) <= sup (downarrow a) by XBOOLE_1:17, YELLOW_0:34;

then sup ((downarrow a) /\ (Join-IRR L)) <= a by WAYBEL_0:34;

hence sup ((downarrow a) /\ (Join-IRR L)) = a by A21, ORDERS_2:2; :: thesis: verum