let L be up-complete Semilattice; 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:]; "\/" ( { (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 S1[ 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 : S1[X] } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L)
by Th9;
A2:
union { X where X is non empty directed Subset of L : S1[X] } is_<=_than "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L)
proof
let a be
Element of
L;
LATTICE3:def 9 ( not a in union { X where X is non empty directed Subset of L : S1[X] } or a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) )
assume
a in union { X where X is non empty directed Subset of L : S1[X] }
;
a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[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 : S1[X] }
by TARSKI:def 4;
consider c being non
empty directed Subset of
L such that A5:
b = c
and A6:
S1[
c]
by A4;
"\/" (
c,
L)
in { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] }
by A6;
then A7:
"\/" (
c,
L)
<= "\/" (
{ ("\/" (X,L)) where X is non empty directed Subset of L : S1[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 : S1[X] } ,
L)
by A7, YELLOW_0:def 2;
verum
end;
ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L
by Th7;
then
"\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[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; verum