let L be lower-bounded meet-continuous LATTICE; :: thesis: for x being Element of L holds meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x
let x be Element of L; :: thesis: meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x
set A = { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ;
set AA = the auxiliary approximating Relation of L;
the auxiliary approximating Relation of L in App L by Def19;
then A1: the auxiliary approximating Relation of L -below x in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ;
A2: meet { I where I is Ideal of L : x <= sup I } = waybelow x by Th34;
A3: meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x by Th43;
set I1 = the Ideal of L;
A4: (DownMap the Ideal of L) . x in { ((DownMap I) . x) where I is Ideal of L : verum } ;
{ ((DownMap I) . x) where I is Ideal of L : verum } c= { (AR -below x) where AR is auxiliary Relation of L : AR in App L }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : verum } or a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } )
assume a in { ((DownMap I) . x) where I is Ideal of L : verum } ; :: thesis: a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L }
then consider I being Ideal of L such that
A5: a = (DownMap I) . x ;
A6: DownMap I is approximating by Th37;
DownMap I in the carrier of (MonSet L) by Th35;
then consider AR being auxiliary Relation of L such that
A7: AR = (Map2Rel L) . (DownMap I) and
A8: for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = DownMap I & x9 in s9 . y9 ) ) by Def15;
A9: ex AR1 being auxiliary approximating Relation of L st AR1 = (Map2Rel L) . (DownMap I) by A6, Th35, Th42;
A10: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A6;
A11: AR -below x c= (DownMap I) . x
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in AR -below x or a in (DownMap I) . x )
assume a in AR -below x ; :: thesis: a in (DownMap I) . x
then [a,x] in AR by Th13;
then ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a & y9 = x & s9 = DownMap I & x9 in s9 . y9 ) by A8;
hence a in (DownMap I) . x ; :: thesis: verum
end;
(DownMap I) . x c= AR -below x
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (DownMap I) . x or a in AR -below x )
assume A12: a in (DownMap I) . x ; :: thesis: a in AR -below x
then reconsider a9 = a as Element of L by A10;
[a9,x] in AR by A8, A12;
hence a in AR -below x ; :: thesis: verum
end;
then A13: AR -below x = (DownMap I) . x by A11;
AR in App L by A7, A9, Def19;
hence a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } by A5, A13; :: thesis: verum
end;
hence meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } c= waybelow x by A3, A4, SETFAM_1:6; :: according to XBOOLE_0:def 10 :: thesis: waybelow x c= meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L }
{ (AR -below x) where AR is auxiliary Relation of L : AR in App L } c= { I where I is Ideal of L : x <= sup I }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } or a in { I where I is Ideal of L : x <= sup I } )
assume a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ; :: thesis: a in { I where I is Ideal of L : x <= sup I }
then consider AR being auxiliary Relation of L such that
A14: a = AR -below x and
A15: AR in App L ;
reconsider AR = AR as auxiliary approximating Relation of L by A15, Def19;
sup (AR -below x) = x by Def17;
hence a in { I where I is Ideal of L : x <= sup I } by A14; :: thesis: verum
end;
hence waybelow x c= meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } by A1, A2, SETFAM_1:6; :: thesis: verum