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

proof

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

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

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

proof

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;

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

end;

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))

proof

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;

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

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;

then (downarrow a) /\ (Join-IRR L) = ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) by A11, XBOOLE_0:def 10;
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;

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;

end;

end;