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