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 (() /\ ()) = b ) holds
sup (() /\ ()) = a

let a be Element of L; :: thesis: ( ( for b being Element of L st b < a holds
sup (() /\ ()) = b ) implies sup (() /\ ()) = a )

assume A1: for b being Element of L st b < a holds
sup (() /\ ()) = b ; :: thesis: sup (() /\ ()) = a
thus sup (() /\ ()) = 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 (() /\ ()) = a
A3: {()} /\ () = {}
proof
set x = the Element of {()} /\ ();
assume A4: {()} /\ () <> {} ; :: thesis: contradiction
then the Element of {()} /\ () in {()} by XBOOLE_0:def 4;
then A5: the Element of {()} /\ () = Bottom L by TARSKI:def 1;
the Element of {()} /\ () in Join-IRR L by ;
hence contradiction by A5, Th10; :: thesis: verum
end;
downarrow a = {()} by ;
hence sup (() /\ ()) = a by ; :: thesis: verum
end;
suppose ( not a in Join-IRR L & a <> Bottom L ) ; :: thesis: sup (() /\ ()) = 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 ;
then A10: y < a by ;
A11: (downarrow a) /\ () c= (() /\ ()) \/ (() /\ ())
proof
let x be Element of L; :: according to LATTICE7:def 1 :: thesis: ( x in () /\ () implies x in (() /\ ()) \/ (() /\ ()) )
set x1 = x;
set y1 = y;
set a1 = a;
set z1 = z;
assume A12: x in () /\ () ; :: thesis: x in (() /\ ()) \/ (() /\ ())
then A13: x in Join-IRR L by XBOOLE_0:def 4;
x in downarrow a by ;
then A14: x <= a by WAYBEL_0:17;
x "/\" a = (x "/\" y) "\/" (x "/\" z) by ;
then x = (x "/\" y) "\/" (x "/\" z) by ;
then ( x = x "/\" y or x = x "/\" z ) by ;
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 () /\ () or x in () /\ () ) by ;
hence x in (() /\ ()) \/ (() /\ ()) by XBOOLE_0:def 3; :: thesis: verum
end;
A15: ( ex_sup_of (() /\ ()) \/ (() /\ ()),L & ex_sup_of () /\ (),L ) by YELLOW_0:17;
A16: ex_sup_of () /\ (),L by YELLOW_0:17;
A17: z <= a by ;
((downarrow y) /\ ()) \/ (() /\ ()) c= () /\ ()
proof
let x be Element of L; :: according to LATTICE7:def 1 :: thesis: ( x in (() /\ ()) \/ (() /\ ()) implies x in () /\ () )
( (downarrow y) /\ () c= () /\ () & () /\ () c= () /\ () ) by ;
then A18: ((downarrow y) /\ ()) \/ (() /\ ()) c= () /\ () by XBOOLE_1:8;
assume x in (() /\ ()) \/ (() /\ ()) ; :: thesis: x in () /\ ()
hence x in () /\ () by A18; :: thesis: verum
end;
then (downarrow a) /\ () = (() /\ ()) \/ (() /\ ()) by ;
then sup (() /\ ()) = (sup (() /\ ())) "\/" (sup (() /\ ())) by ;
then A19: sup (() /\ ()) = y "\/" (sup (() /\ ())) by ;
z < a by ;
hence sup (() /\ ()) = a by A1, A6, A19; :: thesis: verum
end;
suppose A20: a in Join-IRR L ; :: thesis: sup (() /\ ()) = a
a <= a ;
then a in downarrow a by WAYBEL_0:17;
then a in () /\ () by ;
then A21: a <= sup (() /\ ()) by ;
( ex_sup_of () /\ (),L & ex_sup_of downarrow a,L ) by YELLOW_0:17;
then sup (() /\ ()) <= sup () by ;
then sup (() /\ ()) <= a by WAYBEL_0:34;
hence sup (() /\ ()) = a by ; :: thesis: verum
end;
end;
end;