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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MIRRS L or x in D )
assume x in MIRRS L ; :: thesis: x in D
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-meet-irreducible ;
assume A4: not x in D ; :: thesis: contradiction
reconsider x = x as Element of L by A2;
set D9 = { 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 ) } ;
A5: 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 x9 being Element of L st
( x9 = x & x9 in D & x [= x9 ) ;
hence contradiction by A4; :: thesis: verum
end;
for u being object 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 object ; :: 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 A6: 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 ex u9 being Element of L st
( u9 = u & u9 in D & x [= u9 ) ;
hence u in { d where d is Element of L : ( x [= d & d <> x ) } by A5, A6; :: 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 ) } ;
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:45;
then A7: "/\" ( { 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 q9 being Element of L st
( q9 = q & x [= q9 & q9 <> 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 A8: x [= "/\" ( { d where d is Element of L : ( x [= d & d <> x ) } ,L) by LATTICE3:39;
x9 *' <> x9 by A3;
hence contradiction by A2, A7, A8, LATTICES:8; :: thesis: verum