let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (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) = "\/" ((union { 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: "\/" ( { (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) = "\/" ((union { 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)

defpred S_{1}[ set ] means ex x being Element of L st

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

A1: "\/" ( { (sup X) where X is non empty directed Subset of L : S_{1}[X] } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : S_{1}[X] } ),L)
by Th9;

A2: union { X where X is non empty directed Subset of L : S_{1}[X] } is_<=_than "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L)
_{1}[X] } ,L
by Th7;

then "\/" ((union { X where X is non empty directed Subset of L : S_{1}[X] } ),L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L)
by A2, YELLOW_0:def 9;

hence "\/" ( { (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) = "\/" ((union { 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 A1, ORDERS_2:2; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { 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: "\/" ( { (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) = "\/" ((union { 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)

defpred S

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

A1: "\/" ( { (sup X) where X is non empty directed Subset of L : S

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

proof

ex_sup_of union { X where X is non empty directed Subset of L : S
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in union { X where X is non empty directed Subset of L : S_{1}[X] } or a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L) )

assume a in union { X where X is non empty directed Subset of L : S_{1}[X] }
; :: thesis: a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L)

then consider b being set such that

A3: a in b and

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

consider c being non empty directed Subset of L such that

A5: b = c and

A6: S_{1}[c]
by A4;

"\/" (c,L) in { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] }
by A6;

then A7: "\/" (c,L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L)
by Th8, YELLOW_4:1;

ex_sup_of c,L by WAYBEL_0:75;

then a <= "\/" (c,L) by A3, A5, YELLOW_4:1;

hence a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[X] } ,L)
by A7, YELLOW_0:def 2; :: thesis: verum

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

then consider b being set such that

A3: a in b and

A4: b in { X where X is non empty directed Subset of L : S

consider c being non empty directed Subset of L such that

A5: b = c and

A6: S

"\/" (c,L) in { ("\/" (X,L)) where X is non empty directed Subset of L : S

then A7: "\/" (c,L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S

ex_sup_of c,L by WAYBEL_0:75;

then a <= "\/" (c,L) by A3, A5, YELLOW_4:1;

hence a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S

then "\/" ((union { X where X is non empty directed Subset of L : S

hence "\/" ( { (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) = "\/" ((union { 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 A1, ORDERS_2:2; :: thesis: verum