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 z' being Element of (InclPoset (Ids L)) st x <= z' & y <= z' holds
z <= z' ) )

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 z' being Element of (InclPoset (Ids L)) st x <= z' & y <= z' holds
z <= z' ) )
consider Z being Subset of L such that
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 ) ) } and
A1: ex_sup_of {x,y}, InclPoset (Ids L) and
x "\/" y = downarrow Z by Th46;
take x "\/" y ; :: thesis: ( x <= x "\/" y & y <= x "\/" y & ( for z' being Element of (InclPoset (Ids L)) st x <= z' & y <= z' holds
x "\/" y <= z' ) )
thus ( x <= x "\/" y & y <= x "\/" y & ( for z' being Element of (InclPoset (Ids L)) st x <= z' & y <= z' holds
x "\/" y <= z' ) ) by A1, YELLOW_0:18; :: thesis: verum

end;

hence InclPoset (Ids L) is with_suprema by LATTICE3:def 10; :: thesis: verum