let L be with_suprema Poset; :: thesis: for x, y being Element of (InclPoset (Ids L))
for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)
let x, y be Element of (InclPoset (Ids L)); :: thesis: for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)
let X, Y be Subset of L; :: thesis: ( x = X & y = Y implies x "\/" y = downarrow (X "\/" Y) )
assume A1: ( x = X & y = Y ) ; :: thesis: x "\/" y = downarrow (X "\/" Y)
consider Z being Subset of L such that
A2: 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
ex_sup_of {x,y}, InclPoset (Ids L) and
A3: x "\/" y = downarrow Z by YELLOW_2:46;
reconsider X1 = X, Y1 = Y as non empty directed Subset of L by A1, YELLOW_2:43;
reconsider d = downarrow (X1 "\/" Y1) as Element of (InclPoset (Ids L)) by YELLOW_2:43;
A4: d <= d ;
( X c= d & Y c= d ) by Th29;
then ( x <= d & y <= d ) by A1, YELLOW_1:3;
then x "\/" y <= d "\/" d by YELLOW_3:3;
then x "\/" y <= d by A4, YELLOW_0:24;
hence x "\/" y c= downarrow (X "\/" Y) by YELLOW_1:3; :: according to XBOOLE_0:def 10 :: thesis: downarrow (X "\/" Y) c= x "\/" y
X "\/" Y c= Z

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in X "\/" Y or q in Z )
assume q in X "\/" Y ; :: thesis: q in Z
then consider s, t being Element of L such that
A5: ( q = s "\/" t & s in X & t in Y ) ;
thus q in Z by A1, A2, A5; :: thesis: verum

end;

hence downarrow (X "\/" Y) c= x "\/" y by A3, YELLOW_3:6; :: thesis: verum