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 } ;
consider AA being auxiliary approximating Relation of L;
AA in App L by Def20;
then A1: AA -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;
consider I1 being Ideal of L;
A4: (DownMap I1) . 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 set ; :: 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;
A7: DownMap I in the carrier of (MonSet L) by Th35;
then consider AR being auxiliary Relation of L such that
A8: ( AR = (Map2Rel L) . (DownMap I) & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = DownMap I & x' in s' . y' ) ) ) ) by Def16;
consider AR1 being auxiliary approximating Relation of L such that
A9: AR1 = (Map2Rel L) . (DownMap I) by A6, A7, Th42;
consider ii being Subset of L such that
A10: ( ii = (DownMap I) . x & x = sup ii ) by A6, Def19;
A11: AR -below x = (DownMap I) . x

proof

thus AR -below x c= (DownMap I) . x :: according to XBOOLE_0:def 10 :: thesis: (DownMap I) . x c= AR -below x

proof

let a be set ; :: 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 consider x', y' being Element of L, s' being Function of L,(InclPoset (Ids L)) such that
A12: ( x' = a & y' = x & s' = DownMap I & x' in s' . y' ) by A8;
thus a in (DownMap I) . x by A12; :: thesis: verum

end;

thus (DownMap I) . x c= AR -below x :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (DownMap I) . x or a in AR -below x )
assume A13: a in (DownMap I) . x ; :: thesis: a in AR -below x
then reconsider a' = a as Element of L by A10;
[a',x] in AR by A8, A13;
hence a in AR -below x ; :: thesis: verum

end;

end;

AR in App L by A8, A9, Def20;
hence a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } by A5, A11; :: 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:7; :: 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 }
thus waybelow x c= meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } :: thesis: verum

proof

{ (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 set ; :: 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 & AR in App L ) ;
reconsider AR = AR as auxiliary approximating Relation of L by A14, Def20;
sup (AR -below x) = x by Def18;
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:7; :: thesis: verum

end;