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

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

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

proof

let a be Element of L; :: thesis: a = "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,L)
set X = { d where d is Element of L : ( d in D & a [= d ) } ;
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 & a [= d ) }

proof

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

end;

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

proof

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

end;

then a is_less_than { d where d is Element of L : ( d in D & a [= d ) } by LATTICE3:def 16;
then a [= "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,L) by LATTICE3:39;
hence a = "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,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 & a [= d ) } ,L) ) implies D is infimum-dense )

assume A6: for a being Element of L holds a = "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,L) ; :: thesis: D is infimum-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 & a [= d ) } ;
for x being object st x in { d where d is Element of L : ( d in D & a [= d ) } holds
x in D

proof

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

end;

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

end;

hence D is infimum-dense ; :: thesis: verum

end;

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