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