let L be up-complete Semilattice; :: thesis: 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:]; :: thesis: 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 S_{1}[ 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 : S_{1}[X] } ;

{ (sup X) where X is non empty directed Subset of L : S_{1}[X] } c= the carrier of L
_{1}[X] } as Subset of L ;

set R = { X where X is non empty directed Subset of L : S_{1}[X] } ;

union { X where X is non empty directed Subset of L : S_{1}[X] } c= the carrier of L
_{1}[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

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by A4, YELLOW_0:15; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L

let D be non empty directed Subset of [:L,L:]; :: thesis: 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 S

( $1 = {x} "/\" D2 & x in D1 );

set A = { (sup X) where X is non empty directed Subset of L : S

{ (sup X) where X is non empty directed Subset of L : S

proof

then reconsider A = { (sup X) where X is non empty directed Subset of L : S
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] } or q in the carrier of L )

assume q in { (sup X) where X is non empty directed Subset of L : S_{1}[X] }
; :: thesis: q in the carrier of L

then ex X being non empty directed Subset of L st

( q = sup X & S_{1}[X] )
;

hence q in the carrier of L ; :: thesis: verum

end;assume q in { (sup X) where X is non empty directed Subset of L : S

then ex X being non empty directed Subset of L st

( q = sup X & S

hence q in the carrier of L ; :: thesis: verum

set R = { X where X is non empty directed Subset of L : S

union { X where X is non empty directed Subset of L : S

proof

then reconsider UR = union { X where X is non empty directed Subset of L : S
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is non empty directed Subset of L : S_{1}[X] } or q in the carrier of L )

assume q in union { X where X is non empty directed Subset of L : S_{1}[X] }
; :: thesis: q in the carrier of L

then consider r being set such that

A1: q in r and

A2: r in { X where X is non empty directed Subset of L : S_{1}[X] }
by TARSKI:def 4;

ex s being non empty directed Subset of L st

( r = s & ex x being Element of L st

( s = {x} "/\" D2 & x in D1 ) ) by A2;

hence q in the carrier of L by A1; :: thesis: verum

end;assume q in union { X where X is non empty directed Subset of L : S

then consider r being set such that

A1: q in r and

A2: r in { X where X is non empty directed Subset of L : S

ex s being non empty directed Subset of L st

( r = s & ex x being Element of L st

( s = {x} "/\" D2 & x in D1 ) ) by A2;

hence q in the carrier of L by A1; :: thesis: verum

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

A is_<=_than sup UR
let b be Element of L; :: thesis: ( A is_<=_than b implies sup UR <= b )

assume A5: A is_<=_than b ; :: thesis: sup UR <= b

UR is_<=_than b

end;assume A5: A is_<=_than b ; :: thesis: sup UR <= b

UR is_<=_than b

proof

hence
sup UR <= b
by A3, YELLOW_0:def 9; :: thesis: verum
let k be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not k in UR or k <= b )

assume k in UR ; :: thesis: 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 : S_{1}[X] }
by TARSKI:def 4;

consider s being non empty directed Subset of L such that

A8: k1 = s and

A9: S_{1}[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; :: thesis: verum

end;assume k in UR ; :: thesis: 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 : S

consider s being non empty directed Subset of L such that

A8: k1 = s and

A9: S

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; :: thesis: verum

proof

hence
ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in A or b <= sup UR )

assume b in A ; :: thesis: b <= sup UR

then consider X being non empty directed Subset of L such that

A14: b = sup X and

A15: S_{1}[X]
;

( ex_sup_of X,L & X in { X where X is non empty directed Subset of L : S_{1}[X] } )
by A15, WAYBEL_0:75;

hence b <= sup UR by A3, A14, YELLOW_0:34, ZFMISC_1:74; :: thesis: verum

end;assume b in A ; :: thesis: b <= sup UR

then consider X being non empty directed Subset of L such that

A14: b = sup X and

A15: S

( ex_sup_of X,L & X in { X where X is non empty directed Subset of L : S

hence b <= sup UR by A3, A14, YELLOW_0:34, ZFMISC_1:74; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by A4, YELLOW_0:15; :: thesis: verum