let L be with_suprema Poset; :: thesis:
set P = InclPoset (Ids L);
let x, y be Element of (InclPoset (Ids L)); :: thesis:
reconsider x' = x, y' = y as Ideal of L by Th43;
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:
consider z being Element of x';
z 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 )

proof

let u, v be Element of L; :: thesis:
assume that
A1: u in Z and
A2: v in Z ; :: thesis:
consider p being Element of L such that
A3: p = u and
A4: ( 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 A1;
consider q being Element of L such that
A5: q = v and
A6: ( 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 A2;
A7: 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
A8: p in x and
A9: 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
A10: a in x and
A11: b in y and
A12: q = a "\/" b by A9;
reconsider c = a "\/" p as Element of L ;
take z = c "\/" b; :: thesis:
c in x' by A8, A10, WAYBEL_0:40;
hence z in Z by A11; :: thesis:
A13: ( a <= c & p <= c & c <= z & b <= z ) by YELLOW_0:22;
then ( a <= z & b <= z ) by ORDERS_2:26;
hence ( p <= z & q <= z ) by A12, A13, ORDERS_2:26, YELLOW_0:22; :: thesis:

end;

A14: 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 )

proof

let p, q be Element of L; :: thesis:
assume that
A15: p in y and
A16: 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
A17: a in x and
A18: b in y and
A19: q = a "\/" b by A16;
reconsider c = b "\/" p as Element of L ;
take z = a "\/" c; :: thesis:
c in y' by A15, A18, WAYBEL_0:40;
hence z in Z by A17; :: thesis:
A20: ( b <= c & p <= c & a <= z & c <= z ) by YELLOW_0:22;
then ( a <= z & b <= z ) by ORDERS_2:26;
hence ( p <= z & q <= z ) by A19, A20, ORDERS_2:26, YELLOW_0:22; :: thesis:

end;

per cases by A4, A6;

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

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

end;

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

take p "\/" q ; :: thesis:
thus ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q ) by A3, A5, A22, 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
A23: ( z in Z & p <= z & q <= z ) by A7;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A3, A5, A23; :: thesis:

end;

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

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

end;

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

then consider z being Element of L such that
A25: ( z in y' & p <= z & q <= z ) by WAYBEL_0:def 1;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A3, A5, A25; :: 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
A26: ( z in Z & p <= z & q <= z ) by A14;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A3, A5, A26; :: 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
A27: ( z in Z & q <= z & p <= z ) by A7;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A3, A5, A27; :: 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
A28: ( z in Z & q <= z & p <= z ) by A14;
take z ; :: thesis:
thus ( z in Z & u <= z & v <= z ) by A3, A5, A28; :: 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
A29: ( a in x & b in y & p = a "\/" b ) and
A30: ( c in x & d in y & q = c "\/" d ) ;
reconsider ac = a "\/" c, bd = b "\/" d as Element of L ;
take z = ac "\/" bd; :: thesis:
( ac in x' & bd in y' ) by A29, A30, WAYBEL_0:40;
hence z in Z ; :: thesis:
A31: ( a <= ac & c <= ac & b <= bd & d <= bd & ac <= z & bd <= z ) by YELLOW_0:22;
then ( a <= z & b <= z ) by ORDERS_2:26;
hence u <= z by A3, A29, YELLOW_0:22; :: thesis:
( c <= z & d <= z ) by A31, ORDERS_2:26;
hence v <= z by A5, A30, YELLOW_0:22; :: thesis:

end;

then Z is directed by WAYBEL_0:def 1;
then downarrow Z is Ideal of L ;
then reconsider DZ = downarrow Z as Element of (InclPoset (Ids L)) by Th43;
x c= DZ

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A32: a in x ; :: thesis:
then reconsider a' = a as Element of L by Th44;
( a' in Z & Z c= DZ ) by A32, WAYBEL_0:16;
hence a in DZ ; :: thesis:

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A34: a in y ; :: thesis:
then reconsider a' = a as Element of L by Th44;
( a' in Z & Z c= DZ ) by A34, WAYBEL_0:16;
hence a in DZ ; :: thesis:

end;

then A35: y <= DZ by YELLOW_1:3;
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 ( x <= d & y <= d ) ; :: thesis:
then A36: ( x c= d & y c= d ) by YELLOW_1:3;
DZ c= d

proof

let p be set ; :: 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 p' being Element of L such that
A37: p' = p and
A38: ex u being Element of L st
( p' <= u & u in Z ) ;
consider u being Element of L such that
A39: p' <= u and
A40: u in Z by A38;
consider z being Element of L such that
A41: z = u and
A42: ( 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 A40;

per cases by A42;

suppose z in x ; :: thesis:

then p in x' by A37, A39, A41, WAYBEL_0:def 19;
hence p in d by A36; :: thesis:

end;

suppose z in y ; :: thesis:

then p in y' by A37, A39, A41, WAYBEL_0:def 19;
hence p in d by A36; :: thesis:

end;

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

then consider a, b being Element of L such that
A43: a in x and
A44: b in y and
A45: z = a "\/" b ;
reconsider d' = d as Ideal of L by Th43;
u in d' by A36, A41, A43, A44, A45, WAYBEL_0:40;
hence p in d by A37, A39, WAYBEL_0:def 19; :: thesis:

end;

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

end;

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 A33, A35, YELLOW_0:18; :: thesis: