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 that
A1: x = X and
A2: y = Y ; :: thesis: 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; :: according to XBOOLE_0:def 10 :: thesis: 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
proof
let q be object ; :: 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 ex s, t being Element of L st
( q = s "\/" t & s in X & t in Y ) ;
hence q in Z by A1, A2, A4; :: thesis: verum
end;
hence downarrow (X "\/" Y) c= x "\/" y by A5, YELLOW_3:6; :: thesis: verum