set P = InclPoset (Ids L);
for x, y being Element of (InclPoset (Ids L)) ex z being Element of (InclPoset (Ids L)) st
( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
z <= z9 ) )

proof

let x, y be Element of (InclPoset (Ids L)); :: thesis: ex z being Element of (InclPoset (Ids L)) st
( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
z <= z9 ) )
take x "\/" y ; :: thesis: ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
x "\/" y <= z9 ) )
ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) by Th44;
hence ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
x "\/" y <= z9 ) ) by YELLOW_0:18; :: thesis: verum

end;

hence InclPoset (Ids L) is with_suprema ; :: thesis: verum