let L be complete noetherian Lattice; :: thesis: JIRRS L is supremum-dense
defpred S1[ Element of (LattPOSet L)] means ex D9 being Subset of (JIRRS L) st % $1 = "\/" (D9,L);
A1: 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
S1[y] ) holds
S1[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
S1[y] ) implies S1[x] )
set X = { d where d is Element of L : ( d [= % x & d <> % x ) } ;
A2: 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 A3: ex u9 being Element of L st
( u9 = u & u9 [= % x & % x <> u9 ) ;
A4: % x = x by LATTICE3:def 4;
then (% x) % = x by LATTICE3:def 3;
then u % <= x by A3, LATTICE3:7;
hence ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) ) by A3, A4, LATTICE3:def 3, ORDERS_2:def 5; :: thesis: verum
end;
assume A5: for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S1[y] ; :: thesis: S1[x]
A6: for u being Element of L st u in { d where d is Element of L : ( d [= % x & d <> % x ) } holds
S1[u % ]
proof
let u be Element of L; :: thesis: ( u in { d where d is Element of L : ( d [= % x & d <> % x ) } implies S1[u % ] )
assume u in { d where d is Element of L : ( d [= % x & d <> % x ) } ; :: thesis: S1[u % ]
then ( u % <> x & [(u %),x] in the InternalRel of (LattPOSet L) ) by A2;
hence S1[u % ] by A5; :: thesis: verum
end;
per cases ( % x is completely-join-irreducible or not % x is completely-join-irreducible ) ;
suppose A8: not % x is completely-join-irreducible ; :: thesis: S1[x]
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 D9 = 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) ) } ;
A9: *' (% x) = % x by A8;
A10: 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 A11: 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 A12: q in { d where d is Element of L : ( d [= % x & d <> % x ) } ; :: thesis: q [= r
then consider D being Subset of (JIRRS L) such that
A13: % (q %) = "\/" (D,L) by A6;
q % = q by LATTICE3:def 3;
then A14: q = "\/" (D,L) by A13, LATTICE3:def 4;
for v being object 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 object ; :: 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 A15: 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 A12, A13, A14;
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 A15, 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) ) } ;
then for p being Element of L st p in D holds
p [= r by A11, LATTICE3:def 17;
then D is_less_than r by LATTICE3:def 17;
hence q [= r by A14, 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;
for v being object 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 object ; :: 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 v9 being set such that
A16: v in v9 and
A17: v9 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;
ex H being Subset of (JIRRS L) st
( H = v9 & 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 A17;
hence v in JIRRS L by A16; :: thesis: verum
end;
then 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 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
A19: q in h and
A20: 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;
ex h9 being Subset of (JIRRS L) st
( h9 = h & ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( d [= % x & d <> % x ) } & % u = "\/" (h9,L) ) ) by A20;
then consider u being Element of (LattPOSet L) such that
A21: % u in { d where d is Element of L : ( d [= % x & d <> % x ) } and
A22: % u = "\/" (h,L) ;
h is_less_than % u by A22, LATTICE3:def 21;
then A23: q [= % u by A19, 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 A21, LATTICE3:def 17;
hence q [= % x by A23, LATTICES:7; :: thesis: verum
end;
then 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;
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 A10, LATTICE3:def 21;
hence S1[x] by A18; :: thesis: verum
end;
end;
end;
A24: LattPOSet L is well_founded by Def3;
A25: for x being Element of (LattPOSet L) holds S1[x] from WELLFND1:sch 3(A1, A24);
 for a being Element of L ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L)
proof
let a be Element of L; :: thesis: ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L)
% (a %) = a % by LATTICE3:def 4
.= a by LATTICE3:def 3 ;
hence ex D9 being Subset of (JIRRS L) st a = "\/" (D9,L) by A25; :: thesis: verum
end;
hence JIRRS L is supremum-dense ; :: thesis: verum