let L be complete Lattice; :: thesis: for D being Subset of L holds
( D is supremum-dense iff for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L )
let D be Subset of L; :: thesis: ( D is supremum-dense iff for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L )

A1: now

assume A2: D is supremum-dense ; :: thesis: for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L
thus for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L :: thesis: verum

proof

let a be Element of L; :: thesis: a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L
set X = { d where d is Element of L : ( d in D & d [= a ) } ;
consider D' being Subset of D such that
A3: a = "\/" D',L by A2, Def13;
for x being set st x in D' holds
x in { d where d is Element of L : ( d in D & d [= a ) }

proof

let x be set ; :: thesis: ( x in D' implies x in { d where d is Element of L : ( d in D & d [= a ) } )
assume A4: x in D' ; :: thesis: x in { d where d is Element of L : ( d in D & d [= a ) }
then x in D ;
then reconsider x = x as Element of L ;
D' is_less_than a by A3, LATTICE3:def 21;
then x [= a by A4, LATTICE3:def 17;
hence x in { d where d is Element of L : ( d in D & d [= a ) } by A4; :: thesis: verum

end;

then D' c= { d where d is Element of L : ( d in D & d [= a ) } by TARSKI:def 3;
then A5: a [= "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L by A3, LATTICE3:46;
for q being Element of L st q in { d where d is Element of L : ( d in D & d [= a ) } holds
q [= a

proof

let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( d in D & d [= a ) } implies q [= a )
assume q in { d where d is Element of L : ( d in D & d [= a ) } ; :: thesis: q [= a
then ex q' being Element of L st
( q' = q & q' in D & q' [= a ) ;
hence q [= a ; :: thesis: verum

end;

then { d where d is Element of L : ( d in D & d [= a ) } is_less_than a by LATTICE3:def 17;
then "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L [= a by LATTICE3:def 21;
hence a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L by A5, LATTICES:26; :: thesis: verum

end;

end;

now

assume A6: for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L ; :: thesis: D is supremum-dense
for a being Element of L ex D' being Subset of D st a = "\/" D',L

proof

let a be Element of L; :: thesis: ex D' being Subset of D st a = "\/" D',L
set X = { d where d is Element of L : ( d in D & d [= a ) } ;
for x being set st x in { d where d is Element of L : ( d in D & d [= a ) } holds
x in D

proof

let x be set ; :: thesis: ( x in { d where d is Element of L : ( d in D & d [= a ) } implies x in D )
assume x in { d where d is Element of L : ( d in D & d [= a ) } ; :: thesis: x in D
then ex x' being Element of L st
( x' = x & x' in D & x' [= a ) ;
hence x in D ; :: thesis: verum

end;

then A7: { d where d is Element of L : ( d in D & d [= a ) } is Subset of D by TARSKI:def 3;
a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L by A6;
hence ex D' being Subset of D st a = "\/" D',L by A7; :: thesis: verum

end;

hence D is supremum-dense by Def13; :: thesis: verum

end;

hence ( D is supremum-dense iff for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L ) by A1; :: thesis: verum