let L be complete co-noetherian Lattice; :: thesis: MIRRS L is infimum-dense
defpred S₁[ Element of ((LattPOSet L) ~ )] means ex D' being Subset of (MIRRS L) st $1 = ("/\" D',L) % ;
A1: (LattPOSet L) ~ is well_founded by Def4;
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 : ( % (~ x) [= d & d <> % (~ x) ) } ;
A4: 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) ~ ) ) )
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 consider u' being Element of L such that
A5: ( u' = u & % (~ x) [= u' & % (~ x) <> u' ) ;
A6: (% (~ x)) % <= u % by A5, LATTICE3:7;
((% (~ x)) % ) ~ = (% (~ x)) % by LATTICE3:def 6
.= % (~ x) by LATTICE3:def 3
.= ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
then A7: (u % ) ~ <= x by A6, LATTICE3:9;
A8: % (~ x) = ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
(u % ) ~ = u % by LATTICE3:def 6
.= u by LATTICE3:def 3 ;
hence ( (u % ) ~ <> x & [((u % ) ~ ),x] in the InternalRel of ((LattPOSet L) ~ ) ) by A5, A7, A8, ORDERS_2:def 9; :: thesis: verum

end;

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

proof

let u be Element of L; :: thesis: ( u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } implies S₁[(u % ) ~ ] )
assume u in { d where d is Element of L : ( % (~ x) [= d & 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-meet-irreducible or not % (~ x) is completely-meet-irreducible ) ;

suppose % (~ x) is completely-meet-irreducible ; :: thesis: S₁[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 A10: {(% (~ 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 S₁[x] by A10; :: thesis: verum

end;

suppose not % (~ x) is completely-meet-irreducible ; :: thesis: S₁[x]

then A11: (% (~ x)) *' = % (~ x) by Def8;
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 D' = 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 ) } ;
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 v' being set such that
A12: ( v in v' & v' 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;
consider H being Subset of (MIRRS L) such that
A13: ( H = v' & 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 A12;
thus v in MIRRS L by A12, A13; :: thesis: verum

end;

then A14: 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;
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
A15: ( q in h & 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;
consider h' being Subset of (MIRRS L) such that
A16: ( h' = h & 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 A15;
consider u being Element of (LattPOSet L) such that
A17: ( % u in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } & % u = "/\" h,L ) by A16;
% u is_less_than h by A17, LATTICE3:34;
then A18: % u [= q by A15, 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 A17, LATTICE3:def 16;
hence % (~ x) [= q by A18, LATTICES:25; :: thesis: verum

end;

then A19: % (~ 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;
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 A20: 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 A21: q in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } ; :: thesis: r [= q
A22: q % = q by LATTICE3:def 3;
consider D being Subset of (MIRRS L) such that
A23: (q % ) ~ = ("/\" D,L) % by A9, A21;
A24: q = (q % ) ~ by A22, LATTICE3:def 6
.= "/\" D,L by A23, 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 ) } )
assume A25: 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 ) }
A26: % (q % ) in { d where d is Element of L : ( % (~ x) [= d & d <> % (~ x) ) } by A21, A22, LATTICE3:def 4;
(q % ) ~ = q % by LATTICE3:def 6
.= % (q % ) by LATTICE3:def 4 ;
then % (q % ) = "/\" D,L by A23, LATTICE3:def 3;
then 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 A26;
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 A25, 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 A20, LATTICE3:def 16;
then r is_less_than D by LATTICE3:def 16;
hence r [= q by A24, 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;

then A27: % (~ 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 A19, LATTICE3:34;
A28: % (~ x) = ~ x by LATTICE3:def 4
.= x by LATTICE3:def 7 ;
("/\" (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;
hence S₁[x] by A14, A27, A28; :: thesis: verum

end;

end;

end;

A29: 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 (MIRRS L) st a = "/\" D',L

proof

let a be Element of L; :: thesis: ex D' being Subset of (MIRRS L) st a = "/\" D',L
(LattPOSet L) ~ = RelStr(# the carrier of (LattPOSet L),(the InternalRel of (LattPOSet L) ~ ) #) by LATTICE3:def 5;
then reconsider a' = a % as Element of ((LattPOSet L) ~ ) ;
consider D' being Subset of (MIRRS L) such that
A30: a' = ("/\" D',L) % by A29;
a % = a by LATTICE3:def 3;
hence ex D' being Subset of (MIRRS L) st a = "/\" D',L by A30, LATTICE3:def 3; :: thesis: verum

end;

hence MIRRS L is infimum-dense by Def14; :: thesis: verum