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 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
A3: a % = "/\" Y,(LattPOSet L) by A2, WAYBEL_6:15;
A4: 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;

A5: a % is_<=_than Y by A3, YELLOW_0:33;
reconsider Y = Y as Subset of (LattPOSet L) by A4, TARSKI:def 3;
A6: 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 A7: 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 A8: b [= % u by A7, LATTICE3:def 16;
(% u) % = % u by LATTICE3:def 3
.= u by LATTICE3:def 4 ;
hence b % <= u by A8, LATTICE3:7; :: thesis: verum

end;

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

end;

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
A9: x = % x' and
A10: x' in Y ;
x' in D % by A10;
then consider y being Element of L such that
A11: x' = y % and
A12: y in D ;
x = y % by A9, A11, LATTICE3:def 4
.= y by LATTICE3:def 3 ;
hence x in D by A12; :: thesis: verum

end;

then A13: % Y is Subset of D 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
A14: q = % q' and
A15: q' in Y ;
A16: q' = % q' by LATTICE3:def 4
.= (% q') % by LATTICE3:def 3 ;
a % <= q' by A5, A15, LATTICE3:def 8;
hence a [= q by A14, A16, LATTICE3:7; :: thesis: verum

end;

then a is_less_than % Y by LATTICE3:def 16;
then a = "/\" (% Y),L by A6, LATTICE3:34;
hence ex D' being Subset of D st a = "/\" D',L by A13; :: thesis: verum

end;

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

end;

now

assume A17: 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
A18: % a = "/\" D',L by A17, Def14;
A19: 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;

A20: % a is_less_than D' by A18, LATTICE3:34;
reconsider D' = D' as Subset of L by A19, TARSKI:def 3;
A21: 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 )
A22: b = % b by LATTICE3:def 4
.= (% b) % by LATTICE3:def 3 ;
assume A23: D' % is_>=_than b ; :: thesis: b <= a
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 A23, LATTICE3:def 8;
hence % b [= u by A22, LATTICE3:7; :: thesis: verum

end;

then % b is_less_than D' by LATTICE3:def 16;
then A24: % b [= % a by A18, LATTICE3:34;
a = % a by LATTICE3:def 4
.= (% a) % by LATTICE3:def 3 ;
hence b <= a by A22, A24, LATTICE3:7; :: thesis: verum

end;

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 A25: D' % is Subset of (D % ) 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 )
A26: (% a) % = % a by LATTICE3:def 3
.= a by LATTICE3:def 4 ;
assume u in D' % ; :: thesis: a <= u
then consider u' being Element of L such that
A27: u = u' % and
A28: u' in D' ;
% a [= u' by A20, A28, LATTICE3:def 16;
hence a <= u by A27, A26, LATTICE3:7; :: thesis: verum

end;

then D' % is_>=_than a by LATTICE3:def 8;
then a = "/\" (D' % ),(LattPOSet L) by A21, YELLOW_0:33;
hence ex Y being Subset of (D % ) st a = "/\" Y,(LattPOSet L) by A25; :: thesis: verum

end;

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

end;

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