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

reconsider a = downarrow (finsups (union X)) as Element of (InclPoset (Ids L)) by YELLOW_2:41;

A1: union X c= sup X by Lm1, YELLOW_0:17;

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

let X be Subset of (InclPoset (Ids L)); :: thesis: sup X = downarrow (finsups (union X))

reconsider a = downarrow (finsups (union X)) as Element of (InclPoset (Ids L)) by YELLOW_2:41;

A1: union X c= sup X by Lm1, YELLOW_0:17;

A2: now :: thesis: for b being Element of (InclPoset (Ids L)) st b is_>=_than X holds

a <= b

A3:
union X c= downarrow (finsups (union X))
by WAYBEL_0:61;a <= b

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

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

then downarrow (finsups (union X)) c= b1 by WAYBEL_0:61;

hence a <= b by YELLOW_1:3; :: thesis: verum

end;reconsider b1 = b as Ideal of L by YELLOW_2:41;

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

then downarrow (finsups (union X)) c= b1 by WAYBEL_0:61;

hence a <= b by YELLOW_1:3; :: thesis: verum

now :: thesis: for b being Element of (InclPoset (Ids L)) st b in X holds

b <= a

then
a is_>=_than X
;b <= a

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

then b c= downarrow (finsups (union X)) by A3;

hence b <= a by YELLOW_1:3; :: thesis: verum

end;assume b in X ; :: thesis: b <= a

then b c= union X by ZFMISC_1:74;

then b c= downarrow (finsups (union X)) by A3;

hence b <= a by YELLOW_1:3; :: thesis: verum

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