let L be complete Lattice; :: thesis: for D being Subset of L st D is infimum-dense holds
MIRRS L c= D
let D be Subset of L; :: thesis: ( D is infimum-dense implies MIRRS L c= D )
assume A1: D is infimum-dense ; :: thesis: MIRRS L c= D
for x being set st x in MIRRS L holds
x in D

proof

let x be set ; :: thesis: ( x in MIRRS L implies x in D )
assume A2: x in MIRRS L ; :: thesis: x in D
assume A3: not x in D ; :: thesis: contradiction
consider x' being Element of L such that
A4: ( x' = x & x' is completely-meet-irreducible ) by A2;
A5: ( x' = x & x' *' <> x' ) by A4, Def8;
reconsider x = x as Element of L by A4;
set D' = { d where d is Element of L : ( d in D & x [= d ) } ;
set X = { d where d is Element of L : ( x [= d & d <> x ) } ;
A6: not x in { d where d is Element of L : ( d in D & x [= d ) }

proof

assume x in { d where d is Element of L : ( d in D & x [= d ) } ; :: thesis: contradiction
then ex x' being Element of L st
( x' = x & x' in D & x [= x' ) ;
hence contradiction by A3; :: thesis: verum

end;

for u being set st u in { d where d is Element of L : ( d in D & x [= d ) } holds
u in { d where d is Element of L : ( x [= d & d <> x ) }

proof

let u be set ; :: thesis: ( u in { d where d is Element of L : ( d in D & x [= d ) } implies u in { d where d is Element of L : ( x [= d & d <> x ) } )
assume u in { d where d is Element of L : ( d in D & x [= d ) } ; :: thesis: u in { d where d is Element of L : ( x [= d & d <> x ) }
then consider u' being Element of L such that
A7: ( u' = u & u' in D & x [= u' ) ;
reconsider u = u as Element of L by A7;
u <> x by A6, A7;
hence u in { d where d is Element of L : ( x [= d & d <> x ) } by A7; :: thesis: verum

end;

then { d where d is Element of L : ( d in D & x [= d ) } c= { d where d is Element of L : ( x [= d & d <> x ) } by TARSKI:def 3;
then "/\" { d where d is Element of L : ( x [= d & d <> x ) } ,L [= "/\" { d where d is Element of L : ( d in D & x [= d ) } ,L by LATTICE3:46;
then A8: "/\" { d where d is Element of L : ( x [= d & d <> x ) } ,L [= x by A1, Th24;
for q being Element of L st q in { d where d is Element of L : ( x [= d & d <> x ) } holds
x [= q

proof

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

end;

then x is_less_than { d where d is Element of L : ( x [= d & d <> x ) } by LATTICE3:def 16;
then x [= "/\" { d where d is Element of L : ( x [= d & d <> x ) } ,L by LATTICE3:40;
hence contradiction by A5, A8, LATTICES:26; :: thesis: verum

end;

hence MIRRS L c= D by TARSKI:def 3; :: thesis: verum