let L be lower-bounded sup-Semilattice; :: thesis: for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))
let X be Subset of (InclPoset (Ids L)); :: thesis: sup X = downarrow (finsups (union X))
A1: ( union X c= downarrow (finsups (union X)) & ( for I being Ideal of L st union X c= I holds
downarrow (finsups (union X)) c= I ) ) by WAYBEL_0:61;
ex_sup_of X, InclPoset (Ids L) by YELLOW_0:17;
then A2: union X c= sup X by Lm1;
reconsider a = downarrow (finsups (union X)) as Element of (InclPoset (Ids L)) by YELLOW_2:43;

now

let b be Element of (InclPoset (Ids L)); :: thesis: ( b in X implies b <= a )
assume b in X ; :: thesis: b <= a
then b c= union X by ZFMISC_1:92;
then b c= downarrow (finsups (union X)) by A1, XBOOLE_1:1;
hence b <= a by YELLOW_1:3; :: thesis: verum

end;

then A3: a is_>=_than X by LATTICE3:def 9;

now

let b be Element of (InclPoset (Ids L)); :: thesis: ( b is_>=_than X implies a <= b )
reconsider b1 = b as Ideal of L by YELLOW_2:43;
assume b is_>=_than X ; :: thesis: a <= b
then b >= sup X by YELLOW_0:32;
then sup X c= b1 by YELLOW_1:3;
then union X c= b1 by A2, XBOOLE_1:1;
then downarrow (finsups (union X)) c= b1 by WAYBEL_0:61;
hence a <= b by YELLOW_1:3; :: thesis: verum

end;

hence sup X = downarrow (finsups (union X)) by A3, YELLOW_0:32; :: thesis: verum