let L be complete noetherian Lattice; :: thesis: JIRRS L is supremum-dense
defpred S₁[ Element of (LattPOSet L)] means ex D' being Subset of (JIRRS L) st % $1 = "\/" D',L;
A1: LattPOSet L is well_founded by Def3;
A2: for x being Element of (LattPOSet L) st ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ) holds
S₁[x]

proof

let x be Element of (LattPOSet L); :: thesis: ( ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ) implies S₁[x] )
assume A3: for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ; :: thesis: S₁[x]
set X = { d where d is Element of L : ( d [= % x & d <> % x ) } ;
A4: for u being Element of L st u in { d where d is Element of L : ( d [= % x & d <> % x ) } holds
( u % <> x & [(u % ),x] in the InternalRel of (LattPOSet L) )

proof

let u be Element of L; :: thesis: ( u in { d where d is Element of L : ( d [= % x & d <> % x ) } implies ( u % <> x & [(u % ),x] in the InternalRel of (LattPOSet L) ) )
assume u in { d where d is Element of L : ( d [= % x & d <> % x ) } ; :: thesis: ( u % <> x & [(u % ),x] in the InternalRel of (LattPOSet L) )
then consider u' being Element of L such that
A5: ( u' = u & u' [= % x & % x <> u' ) ;
A6: % x = x by LATTICE3:def 4;
then (% x) % = x by LATTICE3:def 3;
then u % <= x by A5, LATTICE3:7;
hence ( u % <> x & [(u % ),x] in the InternalRel of (LattPOSet L) ) by A5, A6, LATTICE3:def 3, ORDERS_2:def 9; :: thesis: verum

end;

A7: for u being Element of L st u in { d where d is Element of L : ( d [= % x & d <> % x ) } holds
S₁[u % ]

proof

let u be Element of L; :: thesis: ( u in { d where d is Element of L : ( d [= % x & d <> % x ) } implies S₁[u % ] )
assume u in { d where d is Element of L : ( d [= % x & d <> % x ) } ; :: thesis: S₁[u % ]
then ( u % <> x & [(u % ),x] in the InternalRel of (LattPOSet L) ) by A4;
hence S₁[u % ] by A3; :: thesis: verum

end;

per cases ( % x is completely-join-irreducible or not % x is completely-join-irreducible ) ;

suppose % x is completely-join-irreducible ; :: thesis: S₁[x]

then % x in { a where a is Element of L : a is completely-join-irreducible } ;
then for y being set st y in {(% x)} holds
y in JIRRS L by TARSKI:def 1;
then A8: {(% x)} is Subset of (JIRRS L) by TARSKI:def 3;
"\/" {(% x)},L = % x by LATTICE3:43;
hence S₁[x] by A8; :: thesis: verum

end;

suppose not % x is completely-join-irreducible ; :: thesis: S₁[x]

then A9: *' (% x) = % x by Def9;
set G = { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ;
set D' = union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ;
for v being set st v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } holds
v in JIRRS L

proof

let v be set ; :: thesis: ( v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } implies v in JIRRS L )
assume v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ; :: thesis: v in JIRRS L
then consider v' being set such that
A10: ( v in v' & v' in { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ) by TARSKI:def 4;
consider H being Subset of (JIRRS L) such that
A11: ( H = v' & ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) ) by A10;
thus v in JIRRS L by A10, A11; :: thesis: verum

end;

then A12: union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } is Subset of (JIRRS L) by TARSKI:def 3;
for q being Element of L st q in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } holds
q [= % x

proof

let q be Element of L; :: thesis: ( q in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } implies q [= % x )
assume q in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ; :: thesis: q [= % x
then consider h being set such that
A13: ( q in h & h in { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ) by TARSKI:def 4;
consider h' being Subset of (JIRRS L) such that
A14: ( h' = h & ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" h',L ) ) by A13;
consider u being Element of (LattPOSet L) such that
A15: ( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" h,L ) by A14;
h is_less_than % u by A15, LATTICE3:def 21;
then A16: q [= % u by A13, LATTICE3:def 17;
{ d where d is Element of L : ( d [= % x & d <> % x ) } is_less_than % x by A9, LATTICE3:def 21;
then % u [= % x by A15, LATTICE3:def 17;
hence q [= % x by A16, LATTICES:25; :: thesis: verum

end;

then A17: union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } is_less_than % x by LATTICE3:def 17;
for r being Element of L st union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } is_less_than r holds
% x [= r

proof

let r be Element of L; :: thesis: ( union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } is_less_than r implies % x [= r )
assume A18: union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } is_less_than r ; :: thesis: % x [= r
for q being Element of L st q in { d where d is Element of L : ( d [= % x & d <> % x ) } holds
q [= r

proof

let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( d [= % x & d <> % x ) } implies q [= r )
assume A19: q in { d where d is Element of L : ( d [= % x & d <> % x ) } ; :: thesis: q [= r
A20: q % = q by LATTICE3:def 3;
consider D being Subset of (JIRRS L) such that
A21: % (q % ) = "\/" D,L by A7, A19;
A22: q = "\/" D,L by A20, A21, LATTICE3:def 4;
for v being set st v in D holds
v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) }

proof

let v be set ; :: thesis: ( v in D implies v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } )
assume A23: v in D ; :: thesis: v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) }
D in { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } by A19, A21, A22;
hence v in union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } by A23, TARSKI:def 4; :: thesis: verum

end;

then D c= union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } by TARSKI:def 3;
then for p being Element of L st p in D holds
p [= r by A18, LATTICE3:def 17;
then D is_less_than r by LATTICE3:def 17;
hence q [= r by A22, LATTICE3:def 21; :: thesis: verum

end;

then { d where d is Element of L : ( d [= % x & d <> % x ) } is_less_than r by LATTICE3:def 17;
hence % x [= r by A9, LATTICE3:def 21; :: thesis: verum

end;

then % x = "\/" (union { H where H is Subset of (JIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" H,L ) } ),L by A17, LATTICE3:def 21;
hence S₁[x] by A12; :: thesis: verum

end;

end;

end;

A24: for x being Element of (LattPOSet L) holds S₁[x] from WELLFND1:sch 3(A2, A1);
for a being Element of L ex D' being Subset of (JIRRS L) st a = "\/" D',L

proof

let a be Element of L; :: thesis: ex D' being Subset of (JIRRS L) st a = "\/" D',L
% (a % ) = a % by LATTICE3:def 4
.= a by LATTICE3:def 3 ;
hence ex D' being Subset of (JIRRS L) st a = "\/" D',L by A24; :: thesis: verum

end;

hence JIRRS L is supremum-dense by Def13; :: thesis: verum