let L be complete co-noetherian Lattice; :: thesis: MIRRS L is infimum-dense
defpred S1[ Element of ((LattPOSet L) ~)] means ex D9 being Subset of (MIRRS 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 : ( % (~ x) [= d & d <> % (~ x) ) } ;
A2: for u being Element of L st u in { d where d is Element of L : ( % (~ x) [= d & 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 : ( % (~ x) [= d & d <> % (~ x) ) } implies ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) )
A3: ((% (~ x)) %) ~ = (% (~ x)) % by LATTICE3:def 6
.= % (~ x) by LATTICE3:def 3
.= ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
assume u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } ; :: thesis: ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) )
then A4: ex u9 being Element of L st
( u9 = u & % (~ x) [= u9 & % (~ x) <> u9 ) ;
then (% (~ x)) % <= u % by LATTICE3:7;
then A5: (u %) ~ <= x by A3, LATTICE3:9;
A6: (u %) ~ = u % by LATTICE3:def 6
.= u by LATTICE3:def 3 ;
% (~ x) = ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
hence ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) by A4, A5, A6, ORDERS_2:def 5; :: thesis: verum
end;
assume A7: for y being Element of ((LattPOSet L) ~) st y <> x & [y,x] in the InternalRel of ((LattPOSet L) ~) holds
S1[y] ; :: thesis: S1[x]
A8: for u being Element of L st u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } holds
S1[(u %) ~ ]
proof
let u be Element of L; :: thesis: ( u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } implies S1[(u %) ~ ] )
assume u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } ; :: thesis: S1[(u %) ~ ]
then ( (u %) ~ <> x & [((u %) ~),x] in the InternalRel of ((LattPOSet L) ~) ) by A2;
hence S1[(u %) ~ ] by A7; :: thesis: verum
end;
per cases ( % (~ x) is completely-meet-irreducible or not % (~ x) is completely-meet-irreducible ) ;
suppose % (~ x) is completely-meet-irreducible ; :: thesis: S1[x]
then % (~ x) in { a where a is Element of L : a is completely-meet-irreducible } ;
then for y being object st y in {(% (~ x))} holds
y in MIRRS L by TARSKI:def 1;
then A9: {(% (~ x))} is Subset of (MIRRS L) by TARSKI:def 3;
("/\" ({(% (~ x))},L)) % = "/\" ({(% (~ x))},L) by LATTICE3:def 3
.= % (~ x) by LATTICE3:42
.= ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
hence S1[x] by A9; :: thesis: verum
end;
suppose A10: not % (~ x) is completely-meet-irreducible ; :: thesis: S1[x]
set G = { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ;
set D9 = union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ;
A11: (% (~ x)) *' = % (~ x) by A10;
A12: for r being Element of L st r is_less_than union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } holds
r [= % (~ x)
proof
let r be Element of L; :: thesis: ( r is_less_than union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } implies r [= % (~ x) )
assume A13: r is_less_than union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ; :: thesis: r [= % (~ x)
for q being Element of L st q in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } holds
r [= q
proof
let q be Element of L; :: thesis: ( q in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } implies r [= q )
assume A14: q in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } ; :: thesis: r [= q
then consider D being Subset of (MIRRS L) such that
A15: (q %) ~ = ("/\" (D,L)) % by A8;
A16: q % = q by LATTICE3:def 3;
for v being object st v in D holds
v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) }
proof
let v be object ; :: thesis: ( v in D implies v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } )
(q %) ~ = q % by LATTICE3:def 6
.= % (q %) by LATTICE3:def 4 ;
then A17: % (q %) = "/\" (D,L) by A15, LATTICE3:def 3;
% (q %) in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } by A14, A16, LATTICE3:def 4;
then A18: D in { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } by A17;
assume v in D ; :: thesis: v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) }
hence v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } by A18, TARSKI:def 4; :: thesis: verum
end;
then D c= union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ;
then for p being Element of L st p in D holds
r [= p by A13, LATTICE3:def 16;
then A19: r is_less_than D by LATTICE3:def 16;
q = (q %) ~ by A16, LATTICE3:def 6
.= "/\" (D,L) by A15, LATTICE3:def 3 ;
hence r [= q by A19, LATTICE3:34; :: thesis: verum
end;
then r is_less_than { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } by LATTICE3:def 16;
hence r [= % (~ x) by A11, LATTICE3:34; :: thesis: verum
end;
for v being object st v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } holds
v in MIRRS L
proof
let v be object ; :: thesis: ( v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } implies v in MIRRS L )
assume v in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ; :: thesis: v in MIRRS L
then consider v9 being set such that
A20: v in v9 and
A21: v9 in { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } by TARSKI:def 4;
ex H being Subset of (MIRRS L) st
( H = v9 & ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) ) by A21;
hence v in MIRRS L by A20; :: thesis: verum
end;
then A22: union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } is Subset of (MIRRS L) by TARSKI:def 3;
A23: % (~ x) = ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
A24: ("/\" ((union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ),L)) % = "/\" ((union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ),L) by LATTICE3:def 3;
for q being Element of L st q in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } holds
% (~ x) [= q
proof
let q be Element of L; :: thesis: ( q in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } implies % (~ x) [= q )
assume q in union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ; :: thesis: % (~ x) [= q
then consider h being set such that
A25: q in h and
A26: h in { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } by TARSKI:def 4;
ex h9 being Subset of (MIRRS L) st
( h9 = h & ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (h9,L) ) ) by A26;
then consider u being Element of (LattPOSet L) such that
A27: % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } and
A28: % u = "/\" (h,L) ;
% u is_less_than h by A28, LATTICE3:34;
then A29: % u [= q by A25, LATTICE3:def 16;
% (~ x) is_less_than { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } by A11, LATTICE3:34;
then % (~ x) [= % u by A27, LATTICE3:def 16;
hence % (~ x) [= q by A29, LATTICES:7; :: thesis: verum
end;
then % (~ x) is_less_than union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } by LATTICE3:def 16;
then % (~ x) = "/\" ((union { H where H is Subset of (MIRRS L) : ex u being Element of (LattPOSet L) st
( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" (H,L) ) } ),L) by A12, LATTICE3:34;
hence S1[x] by A22, A23, A24; :: thesis: verum
end;
end;
end;
A30: (LattPOSet L) ~ is well_founded by Def4;
A31: for x being Element of ((LattPOSet L) ~) holds S1[x] from WELLFND1:sch 3(A1, A30);
 for a being Element of L ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L)
proof
let a be Element of L; :: thesis: ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L)
(LattPOSet L) ~ = RelStr(# the carrier of (LattPOSet L),( the InternalRel of (LattPOSet L) ~) #) by LATTICE3:def 5;
then reconsider a9 = a % as Element of ((LattPOSet L) ~) ;
( ex D9 being Subset of (MIRRS L) st a9 = ("/\" (D9,L)) % & a % = a ) by A31, LATTICE3:def 3;
hence ex D9 being Subset of (MIRRS L) st a = "/\" (D9,L) by LATTICE3:def 3; :: thesis: verum
end;
hence MIRRS L is infimum-dense ; :: thesis: verum