let L be with_suprema Poset; :: thesis:
set P = InclPoset (Ids L);
let x, y be Element of (InclPoset (Ids L)); :: thesis:
defpred S₁[ Element of L] means ( $1 in x or $1 in y or ex a, b being Element of L st
( a in x & b in y & $1 = a "\/" b ) );
reconsider Z = { z where z is Element of L : S₁[z] } as Subset of L from DOMAIN_1:sch 7();
take Z ; :: thesis:
reconsider x9 = x, y9 = y as Ideal of L by Th41;
set z = the Element of x9;
the Element of x9 in Z ;
then reconsider Z = Z as non empty Subset of L ;
set DZ = downarrow Z;
for u, v being Element of L st u in Z & v in Z holds
ex z being Element of L st
( z in Z & u <= z & v <= z )

A1: for p, q being Element of L st p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) holds
ex z being Element of L st
( z in Z & p <= z & q <= z )

let p, q be Element of L; :: thesis:
assume that
A2: p in y and
A3: ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ; :: thesis:
consider a, b being Element of L such that
A4: a in x and
A5: b in y and
A6: q = a "\/" b by A3;
reconsider c = b "\/" p as Element of L ;
take z = a "\/" c; :: thesis:
c in y9 by A2, A5, WAYBEL_0:40;
hence z in Z by A4; :: thesis:
A7: c <= z by YELLOW_0:22;
A8: ( p <= c & a <= z ) by YELLOW_0:22;
b <= c by YELLOW_0:22;
then b <= z by A7, ORDERS_2:3;
hence ( p <= z & q <= z ) by A6, A7, A8, ORDERS_2:3, YELLOW_0:22; :: thesis:

end;

A9: for p, q being Element of L st p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) holds
ex z being Element of L st
( z in Z & p <= z & q <= z )

proof

let p, q be Element of L; :: thesis:
assume that
A10: p in x and
A11: ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ; :: thesis:
consider a, b being Element of L such that
A12: a in x and
A13: b in y and
A14: q = a "\/" b by A11;
reconsider c = a "\/" p as Element of L ;
take z = c "\/" b; :: thesis:
c in x9 by A10, A12, WAYBEL_0:40;
hence z in Z by A13; :: thesis:
A15: c <= z by YELLOW_0:22;
A16: ( p <= c & b <= z ) by YELLOW_0:22;
a <= c by YELLOW_0:22;
then a <= z by A15, ORDERS_2:3;
hence ( p <= z & q <= z ) by A14, A15, A16, ORDERS_2:3, YELLOW_0:22; :: thesis:

end;

let u, v be Element of L; :: thesis:
assume that
A17: u in Z and
A18: v in Z ; :: thesis:
consider p being Element of L such that
A19: p = u and
A20: ( p in x or p in y or ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) by A17;
consider q being Element of L such that
A21: q = v and
A22: ( q in x or q in y or ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) by A18;

per cases by A20, A22;

suppose ( p in x & q in x ) ; :: thesis:

then consider z being Element of L such that
A23: ( z in x9 & p <= z & q <= z ) by WAYBEL_0:def 1;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A23; :: thesis:

end;

suppose A24: ( p in x & q in y ) ; :: thesis:

take p "\/" q ; :: thesis:
thus ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q ) by A19, A21, A24, YELLOW_0:22; :: thesis:

end;

suppose ( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; :: thesis:

then consider z being Element of L such that
A25: ( z in Z & p <= z & q <= z ) by A9;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A25; :: thesis:

end;

suppose A26: ( p in y & q in x ) ; :: thesis:

take q "\/" p ; :: thesis:
thus ( q "\/" p in Z & u <= q "\/" p & v <= q "\/" p ) by A19, A21, A26, YELLOW_0:22; :: thesis:

end;

suppose ( p in y & q in y ) ; :: thesis:

then consider z being Element of L such that
A27: ( z in y9 & p <= z & q <= z ) by WAYBEL_0:def 1;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A27; :: thesis:

end;

suppose ( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; :: thesis:

then consider z being Element of L such that
A28: ( z in Z & p <= z & q <= z ) by A1;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A28; :: thesis:

end;

suppose ( q in x & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) ; :: thesis:

then consider z being Element of L such that
A29: ( z in Z & q <= z & p <= z ) by A9;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A29; :: thesis:

end;

suppose ( q in y & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) ; :: thesis:

then consider z being Element of L such that
A30: ( z in Z & q <= z & p <= z ) by A1;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A19, A21, A30; :: thesis:

end;

suppose ( ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; :: thesis:

then consider a, b, c, d being Element of L such that
A31: ( a in x & b in y ) and
A32: p = a "\/" b and
A33: ( c in x & d in y ) and
A34: q = c "\/" d ;
reconsider ac = a "\/" c, bd = b "\/" d as Element of L ;
take z = ac "\/" bd; :: thesis:
( ac in x9 & bd in y9 ) by A31, A33, WAYBEL_0:40;
hence z in Z ; :: thesis:
A35: ac <= z by YELLOW_0:22;
A36: bd <= z by YELLOW_0:22;
b <= bd by YELLOW_0:22;
then A37: b <= z by A36, ORDERS_2:3;
a <= ac by YELLOW_0:22;
then a <= z by A35, ORDERS_2:3;
hence u <= z by A19, A32, A37, YELLOW_0:22; :: thesis:
d <= bd by YELLOW_0:22;
then A38: d <= z by A36, ORDERS_2:3;
c <= ac by YELLOW_0:22;
then c <= z by A35, ORDERS_2:3;
hence v <= z by A21, A34, A38, YELLOW_0:22; :: thesis:

end;

then Z is directed ;
then reconsider DZ = downarrow Z as Element of (InclPoset (Ids L)) by Th41;
A39: for d being Element of (InclPoset (Ids L)) st d >= x & d >= y holds
DZ <= d

proof

let d be Element of (InclPoset (Ids L)); :: thesis:
assume that
A40: x <= d and
A41: y <= d ; :: thesis:
A42: y c= d by A41, YELLOW_1:3;
A43: x c= d by A40, YELLOW_1:3;
DZ c= d

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in DZ ; :: thesis:
then p in { q where q is Element of L : ex u being Element of L st
( q <= u & u in Z ) } by WAYBEL_0:14;
then consider p9 being Element of L such that
A44: p9 = p and
A45: ex u being Element of L st
( p9 <= u & u in Z ) ;
consider u being Element of L such that
A46: p9 <= u and
A47: u in Z by A45;
consider z being Element of L such that
A48: z = u and
A49: ( 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 ) ) by A47;

per cases by A49;

suppose z in x ; :: thesis:

then p in x9 by A44, A46, A48, WAYBEL_0:def 19;
hence p in d by A43; :: thesis:

end;

suppose z in y ; :: thesis:

then p in y9 by A44, A46, A48, WAYBEL_0:def 19;
hence p in d by A42; :: thesis:

end;

suppose A50: ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ; :: thesis:

reconsider d9 = d as Ideal of L by Th41;
u in d9 by A43, A42, A48, A50, WAYBEL_0:40;
hence p in d by A44, A46, WAYBEL_0:def 19; :: thesis:

end;

hence DZ <= d by YELLOW_1:3; :: thesis:

end;

y c= DZ

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
A51: Z c= DZ by WAYBEL_0:16;
assume A52: a in y ; :: thesis:
then reconsider a9 = a as Element of L by Th42;
a9 in Z by A52;
hence a in DZ by A51; :: thesis:

end;

then A53: y <= DZ by YELLOW_1:3;
x c= DZ

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
A54: Z c= DZ by WAYBEL_0:16;
assume A55: a in x ; :: thesis:
then reconsider a9 = a as Element of L by Th42;
a9 in Z by A55;
hence a in DZ by A54; :: thesis:

end;

then x <= DZ by YELLOW_1:3;
hence ( 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 A53, A39, YELLOW_0:18; :: thesis: