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 :: thesis: ( D is supremum-dense implies for a being Element of L holds a = "\/" ( { d where d is Element of L : ( d in D & d [= a ) } ,L) )

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 D9 being Subset of D such that
A3: a = "\/" (D9,L) by A2;
for x being object st x in D9 holds
x in { d where d is Element of L : ( d in D & d [= a ) }

proof

let x be object ; :: thesis: ( x in D9 implies x in { d where d is Element of L : ( d in D & d [= a ) } )
assume A4: x in D9 ; :: 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 ;
D9 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 D9 c= { d where d is Element of L : ( d in D & d [= a ) } ;
then A5: a [= "\/" ( { d where d is Element of L : ( d in D & d [= a ) } ,L) by A3, LATTICE3:45;
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 q9 being Element of L st
( q9 = q & q9 in D & q9 [= 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:8; :: thesis: verum

end;

end;

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

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 D9 being Subset of D st a = "\/" (D9,L)

proof

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

proof

let x be object ; :: 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 x9 being Element of L st
( x9 = x & x9 in D & x9 [= 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 D9 being Subset of D st a = "\/" (D9,L) by A7; :: thesis: verum

end;

hence D is supremum-dense ; :: 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