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 set st x in JIRRS L holds
x in D

proof

let x be set ; :: thesis: ( x in JIRRS L implies x in D )
assume A2: x in JIRRS 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-join-irreducible ) by A2;
A5: ( x' = x & *' x' <> x' ) by A4, Def9;
reconsider x = x as Element of L by A4;
set D' = { 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 ) } ;
A6: 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 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 & d [= x ) } holds
u in { d where d is Element of L : ( d [= x & d <> x ) }

proof

let u be set ; :: 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 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 consider u' being Element of L such that
A7: ( u' = u & u' in D & u' [= x ) ;
reconsider u = u as Element of L by A7;
u <> x by A6, A7;
hence u in { d where d is Element of L : ( d [= x & d <> x ) } by A7; :: 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 ) } by TARSKI:def 3;
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:46;
then A8: 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 q' being Element of L st
( q' = q & q' [= x & q' <> 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 "\/" { d where d is Element of L : ( d [= x & d <> x ) } ,L [= x by LATTICE3:def 21;
hence contradiction by A5, A8, LATTICES:26; :: thesis: verum

end;

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