let L be complete Lattice; :: thesis: for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )
let D be Subset of L; :: thesis: ( D is infimum-dense iff D % is order-generating )

A1: now

assume A2: D is infimum-dense ; :: thesis: D % is order-generating
for a being Element of (LattPOSet L) ex Y being Subset of (D % ) st a = "/\" Y,(LattPOSet L)

proof

let a be Element of (LattPOSet L); :: thesis: ex Y being Subset of (D % ) st a = "/\" Y,(LattPOSet L)
consider D' being Subset of D such that
A3: % a = "/\" D',L by A2, Def14;
A4: ( % a is_less_than D' & ( for b being Element of L st b is_less_than D' holds
b [= % a ) ) by A3, LATTICE3:34;
for x being set st x in D' holds
x in the carrier of L

proof

let x be set ; :: thesis: ( x in D' implies x in the carrier of L )
assume x in D' ; :: thesis: x in the carrier of L
then x in D ;
hence x in the carrier of L ; :: thesis: verum

end;

then reconsider D' = D' as Subset of L by TARSKI:def 3;
for u being Element of (LattPOSet L) st u in D' % holds
a <= u

proof

let u be Element of (LattPOSet L); :: thesis: ( u in D' % implies a <= u )
assume u in D' % ; :: thesis: a <= u
then consider u' being Element of L such that
A5: ( u = u' % & u' in D' ) ;
A6: % a [= u' by A4, A5, LATTICE3:def 16;
(% a) % = % a by LATTICE3:def 3
.= a by LATTICE3:def 4 ;
hence a <= u by A5, A6, LATTICE3:7; :: thesis: verum

end;

then A7: D' % is_>=_than a by LATTICE3:def 8;
for b being Element of (LattPOSet L) st D' % is_>=_than b holds
b <= a

proof

let b be Element of (LattPOSet L); :: thesis: ( D' % is_>=_than b implies b <= a )
assume A8: D' % is_>=_than b ; :: thesis: b <= a
A9: b = % b by LATTICE3:def 4
.= (% b) % by LATTICE3:def 3 ;
A10: a = % a by LATTICE3:def 4
.= (% a) % by LATTICE3:def 3 ;
for u being Element of L st u in D' holds
% b [= u

proof

let u be Element of L; :: thesis: ( u in D' implies % b [= u )
assume u in D' ; :: thesis: % b [= u
then u % in { (d % ) where d is Element of L : d in D' } ;
then b <= u % by A8, LATTICE3:def 8;
hence % b [= u by A9, LATTICE3:7; :: thesis: verum

end;

then % b is_less_than D' by LATTICE3:def 16;
then % b [= % a by A3, LATTICE3:34;
hence b <= a by A9, A10, LATTICE3:7; :: thesis: verum

end;

then A11: a = "/\" (D' % ),(LattPOSet L) by A7, YELLOW_0:33;
for x being set st x in D' % holds
x in D %

proof

let x be set ; :: thesis: ( x in D' % implies x in D % )
assume x in D' % ; :: thesis: x in D %
then ex x' being Element of L st
( x = x' % & x' in D' ) ;
hence x in D % ; :: thesis: verum

end;

then D' % is Subset of (D % ) by TARSKI:def 3;
hence ex Y being Subset of (D % ) st a = "/\" Y,(LattPOSet L) by A11; :: thesis: verum

end;

hence D % is order-generating by WAYBEL_6:15; :: thesis: verum

end;

now

assume A12: D % is order-generating ; :: 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
consider Y being Subset of (D % ) such that
A13: a % = "/\" Y,(LattPOSet L) by A12, WAYBEL_6:15;
A14: ( a % is_<=_than Y & ( for b being Element of (LattPOSet L) st b is_<=_than Y holds
a % >= b ) ) by A13, YELLOW_0:33;
for x being set st x in Y holds
x in the carrier of (LattPOSet L)

proof

let x be set ; :: thesis: ( x in Y implies x in the carrier of (LattPOSet L) )
assume x in Y ; :: thesis: x in the carrier of (LattPOSet L)
then x in D % ;
hence x in the carrier of (LattPOSet L) ; :: thesis: verum

end;

then reconsider Y = Y as Subset of (LattPOSet L) by TARSKI:def 3;
for q being Element of L st q in % Y holds
a [= q

proof

let q be Element of L; :: thesis: ( q in % Y implies a [= q )
assume q in % Y ; :: thesis: a [= q
then consider q' being Element of (LattPOSet L) such that
A15: ( q = % q' & q' in Y ) ;
A16: a % <= q' by A14, A15, LATTICE3:def 8;
q' = % q' by LATTICE3:def 4
.= (% q') % by LATTICE3:def 3 ;
hence a [= q by A15, A16, LATTICE3:7; :: thesis: verum

end;

then A17: a is_less_than % Y by LATTICE3:def 16;
for b being Element of L st b is_less_than % Y holds
b [= a

proof

let b be Element of L; :: thesis: ( b is_less_than % Y implies b [= a )
assume A18: b is_less_than % Y ; :: thesis: b [= a
for u being Element of (LattPOSet L) st u in Y holds
b % <= u

proof

let u be Element of (LattPOSet L); :: thesis: ( u in Y implies b % <= u )
assume u in Y ; :: thesis: b % <= u
then % u in { (% d) where d is Element of (LattPOSet L) : d in Y } ;
then A19: b [= % u by A18, LATTICE3:def 16;
(% u) % = % u by LATTICE3:def 3
.= u by LATTICE3:def 4 ;
hence b % <= u by A19, LATTICE3:7; :: thesis: verum

end;

then b % is_<=_than Y by LATTICE3:def 8;
then b % <= a % by A13, YELLOW_0:33;
hence b [= a by LATTICE3:7; :: thesis: verum

end;

then A20: a = "/\" (% Y),L by A17, LATTICE3:34;
for x being set st x in % Y holds
x in D

proof

let x be set ; :: thesis: ( x in % Y implies x in D )
assume x in % Y ; :: thesis: x in D
then consider x' being Element of (LattPOSet L) such that
A21: ( x = % x' & x' in Y ) ;
x' in D % by A21;
then consider y being Element of L such that
A22: ( x' = y % & y in D ) ;
x = y % by A21, A22, LATTICE3:def 4
.= y by LATTICE3:def 3 ;
hence x in D by A22; :: thesis: verum

end;

then % Y is Subset of D by TARSKI:def 3;
hence ex D' being Subset of D st a = "/\" D',L by A20; :: thesis: verum

end;

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

end;

hence ( D is infimum-dense iff D % is order-generating ) by A1; :: thesis: verum