let L be with_suprema Poset; for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( 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 )
set P = InclPoset (Ids L);
let x, y be Element of (InclPoset (Ids L)); ex Z being Subset of L st
( 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 )
defpred S1[ 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 : S1[z] } as Subset of L from DOMAIN_1:sch 7();
take
Z
; ( 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 )
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 )
proof
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 )
proof
let p,
q be
Element of
L;
( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st
( z in Z & p <= z & q <= z ) )
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 )
;
ex z being Element of L st
( z in Z & p <= z & q <= z )
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;
( z in Z & p <= z & q <= z )
c in y9
by A2, A5, WAYBEL_0:40;
hence
z in Z
by A4;
( p <= z & q <= z )
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;
verum
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;
( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st
( z in Z & p <= z & q <= z ) )
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 )
;
ex z being Element of L st
( z in Z & p <= z & q <= z )
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;
( z in Z & p <= z & q <= z )
c in x9
by A10, A12, WAYBEL_0:40;
hence
z in Z
by A13;
( p <= z & q <= z )
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;
verum
end;
let u,
v be
Element of
L;
( u in Z & v in Z implies ex z being Element of L st
( z in Z & u <= z & v <= z ) )
assume that A17:
u in Z
and A18:
v in Z
;
ex z being Element of L st
( z in Z & u <= z & v <= z )
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
( ( p in x & q in x ) or ( p in x & q in y ) or ( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) or ( p in y & q in x ) or ( p in y & q in y ) or ( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) or ( q in x & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) or ( q in y & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) or ( 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 ) ) )
by A20, A22;
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 ) )
;
ex z being Element of L st
( z in Z & u <= z & v <= z )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;
( z in Z & u <= z & v <= z )
(
ac in x9 &
bd in y9 )
by A31, A33, WAYBEL_0:40;
hence
z in Z
;
( u <= z & v <= z )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;
v <= z
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;
verum end; end;
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
y c= DZ
then A53:
y <= DZ
by YELLOW_1:3;
x c= DZ
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; verum