let L be complete Lattice; :: thesis: for D being Subset of L st D is supremum-dense holds
JIRRS L c= D
let D be Subset of L; :: thesis: ( D is supremum-dense implies JIRRS L c= D )
assume A1: D is supremum-dense ; :: thesis: JIRRS L c= D
for x being object st x in JIRRS L holds
x in D
proof
let x be object ; :: thesis: ( x in JIRRS L implies x in D )
assume x in JIRRS L ; :: thesis: x in D
then consider x9 being Element of L such that
A2: x9 = x and
A3: x9 is completely-join-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 & d [= x ) } ;
set X = { d where d is Element of L : ( d [= x & d <> x ) } ;
A5: not x in { d where d is Element of L : ( d in D & d [= x ) }
proof
assume x in { d where d is Element of L : ( d in D & d [= x ) } ; :: thesis: contradiction
then ex x9 being Element of L st
( x9 = x & x9 in D & x9 [= x ) ;
hence contradiction by A4; :: thesis: verum
end;
for u being object st u in { d where d is Element of L : ( d in D & d [= x ) } holds
u in { d where d is Element of L : ( d [= x & d <> x ) }
proof
let u be object ; :: thesis: ( u in { d where d is Element of L : ( d in D & d [= x ) } implies u in { d where d is Element of L : ( d [= x & d <> x ) } )
assume A6: u in { d where d is Element of L : ( d in D & d [= x ) } ; :: thesis: u in { d where d is Element of L : ( d [= x & d <> x ) }
then ex u9 being Element of L st
( u9 = u & u9 in D & u9 [= x ) ;
hence u in { d where d is Element of L : ( d [= x & d <> x ) } by A5, A6; :: thesis: verum
end;
then { d where d is Element of L : ( d in D & d [= x ) } c= { d where d is Element of L : ( d [= x & d <> x ) } ;
then "\/" ( { d where d is Element of L : ( d in D & d [= x ) } ,L) [= "\/" ( { d where d is Element of L : ( d [= x & d <> x ) } ,L) by LATTICE3:45;
then A7: x [= "\/" ( { d where d is Element of L : ( d [= x & d <> x ) } ,L) by A1, Th23;
for q being Element of L st q in { d where d is Element of L : ( d [= x & d <> x ) } holds
q [= x
proof
let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( d [= x & d <> x ) } implies q [= x )
assume q in { d where d is Element of L : ( d [= x & d <> x ) } ; :: thesis: q [= x
then ex q9 being Element of L st
( q9 = q & q9 [= x & q9 <> x ) ;
hence q [= x ; :: thesis: verum
end;
then { d where d is Element of L : ( d [= x & d <> x ) } is_less_than x by LATTICE3:def 17;
then A8: "\/" ( { d where d is Element of L : ( d [= x & d <> x ) } ,L) [= x by LATTICE3:def 21;
*' x9 <> x9 by A3;
hence contradiction by A2, A7, A8, LATTICES:8; :: thesis: verum
end;
hence JIRRS L c= D ; :: thesis: verum