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;
A2: now :: thesis: for b being Element of (InclPoset (Ids L)) st b is_>=_than X holds
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;
A3: union X c= downarrow (finsups (union X)) by WAYBEL_0:61;
now :: thesis: for b being Element of (InclPoset (Ids L)) st b in X holds
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;
then a is_>=_than X ;
hence sup X = downarrow (finsups (union X)) by A2, YELLOW_0:32; :: thesis: verum