let L be up-complete Semilattice; for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
let D be non empty directed Subset of [:L,L:]; ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" D2 & x in D1 );
set A = { (sup X) where X is non empty directed Subset of L : S1[X] } ;
{ (sup X) where X is non empty directed Subset of L : S1[X] } c= the carrier of L
then reconsider A = { (sup X) where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set R = { X where X is non empty directed Subset of L : S1[X] } ;
union { X where X is non empty directed Subset of L : S1[X] } c= the carrier of L
then reconsider UR = union { X where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set a = sup UR;
A3:
ex_sup_of UR,L
by Th7;
A4:
for b being Element of L st A is_<=_than b holds
sup UR <= b
proof
let b be
Element of
L;
( A is_<=_than b implies sup UR <= b )
assume A5:
A is_<=_than b
;
sup UR <= b
UR is_<=_than b
proof
let k be
Element of
L;
LATTICE3:def 9 ( not k in UR or k <= b )
assume
k in UR
;
k <= b
then consider k1 being
set such that A6:
k in k1
and A7:
k1 in { X where X is non empty directed Subset of L : S1[X] }
by TARSKI:def 4;
consider s being non
empty directed Subset of
L such that A8:
k1 = s
and A9:
S1[
s]
by A7;
consider x being
Element of
L such that A10:
s = {x} "/\" D2
and
x in D1
by A9;
A11:
{x} "/\" D2 = { (x "/\" d2) where d2 is Element of L : d2 in D2 }
by YELLOW_4:42;
sup s in A
by A9;
then A12:
sup s <= b
by A5;
consider d2 being
Element of
L such that A13:
k = x "/\" d2
and
d2 in D2
by A6, A8, A10, A11;
x "/\" d2 <= sup s
by A6, A8, A10, A13, Th1, YELLOW_4:1;
hence
k <= b
by A13, A12, YELLOW_0:def 2;
verum
end;
hence
sup UR <= b
by A3, YELLOW_0:def 9;
verum
end;
A is_<=_than sup UR
hence
ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
by A4, YELLOW_0:15; verum