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

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

proof

let x be set ; :: thesis: ( x in D' implies x in { d where d is Element of L : ( d in D & a [= d ) } )
assume A4: x in D' ; :: 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 D' 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 D' c= { d where d is Element of L : ( d in D & a [= d ) } by TARSKI:def 3;
then A5: "/\" { d where d is Element of L : ( d in D & a [= d ) } ,L [= a by A3, LATTICE3:46;
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 q' being Element of L st
( q' = q & q' in D & a [= q' ) ;
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:40;
hence a = "/\" { d where d is Element of L : ( d in D & a [= d ) } ,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 & a [= d ) } ,L ; :: thesis: D is infimum-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 & a [= d ) } ;
for x being set st x in { d where d is Element of L : ( d in D & a [= d ) } holds
x in D

proof

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

end;

hence D is infimum-dense by Def14; :: 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