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 9; :: 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 set 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:43
.= ~ 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, Def8;
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 set 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 set ; :: 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 ) } by TARSKI:def 3;
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 set 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 set ; :: 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:25; :: 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 by Def14; :: thesis: verum